∀ {G : Type u_2} [inst : CommGroup G] {g g' : G} [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] {f : ℤ → G},
  HasProd (fun n => f ↑n) g → HasProd (fun n => f (-↑n)) g' → HasProd f (g * g' / f 0)