let V be Z_Module; :: thesis: ( V is_the_direct_sum_of (0). V, (Omega). V & V is_the_direct_sum_of (Omega). V, (0). V )
V is_the_direct_sum_of (0). V, (Omega). V by Th99, Th107;
hence ( V is_the_direct_sum_of (0). V, (Omega). V & V is_the_direct_sum_of (Omega). V, (0). V ) by VECTSP_5:41; :: thesis: verum