{𝕜 : Type u_1} →
  {I : Type u_5} →
    {B : I → Type u_6} →
      [inst : NormedField 𝕜] →
        [inst_1 : (i : I) → NormedRing (B i)] →
          [(i : I) → NormedAlgebra 𝕜 (B i)] → [inst_3 : ∀ (i : I), NormOneClass (B i)] → NormedAlgebra 𝕜 ↥(lp B ⊤)