∀ {α : Type u_1} {R : Type u_3} (M : Type u_4) [inst : TopologicalSpace R] [inst_1 : TopologicalSpace M]
  [inst_2 : AddCommMonoid R] [inst_3 : AddCommMonoid M] {f : α → TrivSqZeroExt R M} {a : TrivSqZeroExt R M},
  HasSum f a → HasSum (fun x => (f x).fst) a.fst