diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index ce8b64fa26..c3166b5229 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -23,6 +23,9 @@
   + lemmas `in_set1`, `inr_in_set_inr`, `inl_in_set_inr`, `mem_image`, `mem_range`, `image_f`
   + lemmas `inr_in_set_inl`, `inl_in_set_inl`
 
+- in `lebesgue_integral_approximation.v`:
+  + lemma `measurable_prod`
+
 ### Changed
 
 - in `pi_irrational`:
diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_approximation.v b/theories/lebesgue_integral_theory/lebesgue_integral_approximation.v
index 4850ce47cb..3572deb58b 100644
--- a/theories/lebesgue_integral_theory/lebesgue_integral_approximation.v
+++ b/theories/lebesgue_integral_theory/lebesgue_integral_approximation.v
@@ -576,8 +576,8 @@ Section measurable_sum.
 Context d (T : measurableType d) (R : realType).
 Implicit Types (D : set T) (f g : T -> R).
 
-Lemma measurable_sum D I s (h : I -> (T -> R)) :
-  (forall n, measurable_fun D (h n)) ->
+Lemma measurable_sum D I s (h : I -> T -> R) :
+  (forall i, measurable_fun D (h i)) ->
   measurable_fun D (fun x => \sum_(i <- s) h i x).
 Proof.
 move=> mh; apply/measurable_EFinP.
@@ -586,6 +586,17 @@ rewrite (_ : _ \o _ = (fun t => \sum_(i <- s) (h i t)%:E)); last first.
 by apply/emeasurable_sum => i; exact/measurable_EFinP.
 Qed.
 
+Lemma measurable_prod D (I : eqType) (s : seq I) (h : I -> T -> R) :
+  (forall i, i \in s -> measurable_fun D (h i)) ->
+  measurable_fun D (fun x => \prod_(i <- s) h i x).
+Proof.
+elim: s => [mh|x y ih mh].
+  by under eq_fun do rewrite big_nil//=; exact: measurable_cst.
+under eq_fun do rewrite big_cons//=; apply: measurable_funM => //.
+- by apply: mh; rewrite mem_head.
+- by apply: ih => n ny; apply: mh; rewrite inE orbC ny.
+Qed.
+
 End measurable_sum.
 
 Section emeasurable_comparison.