let R be Ring; :: thesis: for V being strict RightMod of R holds
( V is_the_direct_sum_of (0). V, (Omega). V & V is_the_direct_sum_of (Omega). V, (0). V )
let V be strict RightMod of R; :: thesis: ( V is_the_direct_sum_of (0). V, (Omega). V & V is_the_direct_sum_of (Omega). V, (0). V )
( ((0). V) + ((Omega). V) = V & (0). V = ((0). V) /\ ((Omega). V) ) by Th13, Th25;
hence V is_the_direct_sum_of (0). V, (Omega). V by Def4; :: thesis: V is_the_direct_sum_of (Omega). V, (0). V
hence V is_the_direct_sum_of (Omega). V, (0). V by Th46; :: thesis: verum