∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {ι : Type u_10} (s : Finset ι) (f : ι → SchwartzMap E F) (x : E),
  (∑ i ∈ s, f i) x = ∑ i ∈ s, (f i) x