∀ {𝕜 : Type u_4} {𝕜' : Type u_5} {D : Type u_1} {E : Type u_2} {G : Type u_3} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedField 𝕜] [inst_3 : NormedField 𝕜'] [inst_4 : NormedAddCommGroup D]
  [inst_5 : NormedSpace ℝ D] [inst_6 : NormedSpace 𝕜 E] [inst_7 : SMulCommClass ℝ 𝕜 E] [inst_8 : NormedAddCommGroup G]
  [inst_9 : NormedSpace 𝕜' G] {σ : 𝕜 →+* 𝕜'} [RingHomIsometric σ] (A : SchwartzMap D E → G)
  (hadd : ∀ (f g : SchwartzMap D E), A (f + g) = A f + A g)
  (hsmul : ∀ (a : 𝕜) (f : SchwartzMap D E), A (a • f) = σ a • A f),
  (∃ s C, 0 ≤ C ∧ ∀ (f : SchwartzMap D E), ‖A f‖ ≤ C * (s.sup (schwartzSeminormFamily 𝕜 D E)) f) →
    Continuous { toFun := fun x => A x, map_add' := hadd, map_smul' := hsmul }.toFun