∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F] {n : ℕ∞} {V : Type u_6} [inst_6 : AddCommGroup V]
  [inst_7 : Module ℝ V] [t : TopologicalSpace V] [inst_8 : IsTopologicalAddGroup V] [inst_9 : ContinuousSMul ℝ V]
  [inst_10 : LocallyConvexSpace ℝ V] [inst_11 : Algebra ℝ 𝕜] [inst_12 : IsScalarTower ℝ 𝕜 F] [inst_13 : Module 𝕜 V]
  [inst_14 : IsScalarTower ℝ 𝕜 V] (toFun toFun_1 : TestFunction Ω F n → V) (e_toFun : toFun = toFun_1)
  (map_add : ∀ (f g : TestFunction Ω F n), toFun (f + g) = toFun f + toFun g)
  (map_smul : ∀ (c : 𝕜) (f : TestFunction Ω F n), toFun (c • f) = c • toFun f)
  (cont :
    ∀ (K : TopologicalSpace.Compacts E) (K_sub_Ω : ↑K ⊆ ↑Ω), Continuous (toFun ∘ TestFunction.ofSupportedIn K_sub_Ω)),
  TestFunction.mkCLM 𝕜 toFun map_add map_smul cont = TestFunction.mkCLM 𝕜 toFun_1 ⋯ ⋯ ⋯