∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α}
  {a : α} {g : γ → α} (e : ↑(Function.support f) ≃ ↑(Function.support g)),
  (∀ (x : ↑(Function.support f)), g ↑(e x) = f ↑x) → (HasSum f a ↔ HasSum g a)