∀ {M : Type u_1} [inst : CommMonoid M] [inst_1 : TopologicalSpace M] [ContinuousMul M] [T2Space M] {f : ℤ → M},
  (Multipliable fun n => f (↑n + 1)) →
    (Multipliable fun n => f (-(↑n + 1))) → ∏' (n : ℤ), f n = (∏' (n : ℕ), f (↑n + 1)) * f 0 * ∏' (n : ℕ), f (-(↑n + 1))