∀ (𝕜 : Type u_5) [inst : NontriviallyNormedField 𝕜] (M₁ : Type u_1) (M₂ : Type u_2) (M₃ : Type u_3) (M₄ : Type u_4)
  [inst_1 : SeminormedAddCommGroup M₁] [inst_2 : NormedSpace 𝕜 M₁] [inst_3 : SeminormedAddCommGroup M₂]
  [inst_4 : NormedSpace 𝕜 M₂] [inst_5 : SeminormedAddCommGroup M₃] [inst_6 : NormedSpace 𝕜 M₃]
  [inst_7 : SeminormedAddCommGroup M₄] [inst_8 : NormedSpace 𝕜 M₄], ContinuousAdd (M₁ × M₃ →L[𝕜] M₂ × M₄)