theorem AEEqFun.mk_sum {α : Type u_1} {E : Type u_2} {ι : Type u_3} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E] {s : Finset ι} {f : ι → α → E} (hf : ∀ i ∈ s, MeasureTheory.AEStronglyMeasurable (f i) μ) : MeasureTheory.AEEqFun.mk (∑ i ∈ s, f i) ⋯ = ∑ i ∈ s.attach, MeasureTheory.AEEqFun.mk (f ↑i) ⋯