let X be RealUnitarySpace; :: thesis: {} is OrthonormalFamily of X
A1: {} is OrthogonalFamily of X by Th2;
for x being Point of X st x in {} holds
x .|. x = 1 ;
hence {} is OrthonormalFamily of X by A1, Def9; :: thesis: verum