let V be Z_Module; :: thesis: ( (0). V is Linear_Compl of (Omega). V & (Omega). V is Linear_Compl of (0). V )
A1: ( V is_the_direct_sum_of (0). V, (Omega). V & V is_the_direct_sum_of (Omega). V, (0). V ) by Th129;
then A2: (Omega). V is with_Linear_Compl ;
(0). V is with_Linear_Compl by A1;
hence ( (0). V is Linear_Compl of (Omega). V & (Omega). V is Linear_Compl of (0). V ) by Def19, A1, A2; :: thesis: verum