∀ {𝕜 : Type u_4} {E : Type u_2} {F : Type u_5} {G : Type u_3} {ι : Type u_1} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : SeminormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] [inst_7 : Fintype ι]
  (f : F →ₗ[𝕜] E [⋀^ι]→ₗ[𝕜] G) (C : ℝ) (H : ∀ (x : F) (m : ι → E), ‖(f x) m‖ ≤ C * ‖x‖ * ∏ i, ‖m i‖) (x : F),
  ‖{ toFun := fun x => (f x).mkContinuous (C * ‖x‖) ⋯, map_add' := ⋯, map_smul' := ⋯ } x‖ ≤ max C 0 * ‖x‖