for X being RealUnitarySpace holds (0. X) .|. (0. X) = 0 by Def2;