(A : Type u_2) →
  (E : Type u_6) →
    [inst : Monoid A] →
      [inst_1 : TopologicalSpace A] →
        [inst_2 : CommGroup E] → [inst_3 : TopologicalSpace E] → [IsTopologicalGroup E] → CommGroup (A →ₜ* E)