∀ {α : Type u_1} {R : Type u_2} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace R] [inst_2 : AddMonoid R]
  [ContinuousAdd R] (f : BoundedContinuousFunction α R) (n : ℕ), Continuous fun b => n • f b