∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} [inst : Ring 𝕜] [inst_1 : Ring 𝕜₂]
  [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : Module 𝕜 E] [inst_5 : Module 𝕜₂ F]
  {σ : 𝕜 →+* 𝕜₂} (f f_1 : E →ₛₗ[σ] F) (e_f : f = f_1) (C C_1 : ℝ) (e_C : C = C_1) (h : ∀ (x : E), ‖f x‖ ≤ C * ‖x‖),
  f.mkContinuous C h = f_1.mkContinuous C_1 ⋯