for V being Z_Module holds
( (0). V is Linear_Compl of (Omega). V & (Omega). V is Linear_Compl of (0). V )