∀ {Ω : Type u_1} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_10} {m : MeasurableSpace β}
  [inst : AddCommMonoid β] [MeasurableAdd₂ β] {f : ℕ → Ω → β},
  ProbabilityTheory.iIndepFun f μ →
    (∀ (i : ℕ), AEMeasurable (f i) μ) → ∀ (n : ℕ), ProbabilityTheory.IndepFun (∑ j ∈ Finset.range n, f j) (f n) μ