for V being RealUnitarySpace holds
( ((0). V) /\ ((Omega). V) = (0). V & ((Omega). V) /\ ((0). V) = (0). V ) by Th18;