∀ (A : Type u_1) (E : Type u_2) [inst : AddMonoid A] [inst_1 : TopologicalSpace A] [inst_2 : AddCommGroup E]
  [inst_3 : TopologicalSpace E] [inst_4 : IsTopologicalAddGroup E] (a b : A →ₜ+ E), a + b = b + a