∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] [T2Space M] [ContinuousAdd M] {f : ℕ → M},
  (Summable fun k => f (2 * k)) →
    (Summable fun k => f (2 * k + 1)) → ∑' (k : ℕ), f (2 * k) + ∑' (k : ℕ), f (2 * k + 1) = ∑' (k : ℕ), f k