(𝕜 : Type u_7) →
  [inst : RCLike 𝕜] →
    (E : Type u_8) →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : InnerProductSpace 𝕜 E] → [FiniteDimensional 𝕜 E] → OrthonormalBasis (Fin (Module.finrank 𝕜 E)) 𝕜 E