theorem Th8: :: RUSUB_6:8

for H being RealUnitarySpace
for G being OrthonormalFamily of H holds G is linearly-independent