∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} [T2Space α]
  [ContinuousAdd α] {ι : Type u_4} {s : Finset ι} {t : ι → Set β},
  (↑s).Pairwise (Function.onFun Disjoint t) →
    (∀ i ∈ s, Summable (f ∘ Subtype.val)) → ∑' (x : ↑(⋃ i ∈ s, t i)), f ↑x = ∑ i ∈ s, ∑' (x : ↑(t i)), f ↑x