∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {ι : Type u_6}
  {m : MeasurableSpace α} {f : α → G} {μ : ι → MeasureTheory.Measure α},
  MeasureTheory.Integrable f (MeasureTheory.Measure.sum μ) →
    HasSum (fun i => ∫ (a : α), f a ∂μ i) (∫ (a : α), f a ∂MeasureTheory.Measure.sum μ)