∀ (𝕜 : Type u_1) (α : Type u_2) (E : Type u_3) (H : Type u_4) {hom : Type u_5} [inst : NormedField 𝕜]
  [inst_1 : AddCommGroup H] [inst_2 : Module 𝕜 H] [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E]
  [inst_5 : TopologicalSpace H] [inst_6 : UniformSpace E] [IsUniformAddGroup E] [ContinuousSMul 𝕜 E] {𝔖 : Set (Set α)}
  [inst_9 : FunLike hom H (α → E)] [LinearMapClass hom 𝕜 H (α → E)] (φ : hom),
  Topology.IsInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ ⇑φ) →
    (∀ (u : H), ∀ s ∈ 𝔖, Bornology.IsVonNBounded 𝕜 (φ u '' s)) → ContinuousSMul 𝕜 H