∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {l : Filter A},
  (∀ (m : A), 0 ≤ m → ‖m‖ < 1 → Filter.Tendsto (fun x => x * m) l (nhds m)) →
    ∀ (m : A), Filter.Tendsto (fun x => x * m) l (nhds m)