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) μ)
: