for X being RealUnitarySpace holds {} is OrthonormalFamily of X