theorem Th3: :: BHSP_5:3

for X being RealUnitarySpace holds {} is OrthonormalFamily of X