∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : ℕ} {E : Fin n → Type u_3}
  [inst_1 : (i : Fin n) → MeasureTheory.MeasureSpace (E i)]
  [∀ (i : Fin n), MeasureTheory.SigmaFinite MeasureTheory.volume] (f : (i : Fin n) → E i → 𝕜),
  ∫ (x : (i : Fin n) → E i), ∏ i, f i (x i) = ∏ i, ∫ (x : E i), f i x