for R being Ring
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 ) by Th9, Th21;