(𝕜 : Type u_8) →
  [inst : NontriviallyNormedField 𝕜] →
    (E : Type u_9) →
      (F : Type u_10) →
        [inst_1 : SeminormedAddCommGroup E] →
          [inst_2 : NormedSpace 𝕜 E] → [inst_3 : SeminormedAddCommGroup F] → [inst_4 : NormedSpace 𝕜 F] → F →ₗᵢ[𝕜] E × F