:: deftheorem Def9 defines OrthonormalFamily BHSP_5:def 9 :
for X being RealUnitarySpace
for b₂ being Subset of X holds
( b₂ is OrthonormalFamily of X iff ( b₂ is OrthogonalFamily of X & ( for x being Point of X st x in b₂ holds
x .|. x = 1 ) ) );