∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {μ : MeasureTheory.Measure X} {ι : Type u_5} [inst_2 : Fintype ι] {s : ι → Set X},
  (∀ (i : ι), MeasurableSet (s i)) →
    Pairwise (Function.onFun Disjoint s) →
      (∀ (i : ι), MeasureTheory.IntegrableOn f (s i) μ) → ∫ (x : X) in ⋃ i, s i, f x ∂μ = ∑ i, ∫ (x : X) in s i, f x ∂μ