for V being RealUnitarySpace holds
( (0). V is Linear_Compl of (Omega). V & (Omega). V is Linear_Compl of (0). V ) by Th39, Def5;