for R being Ring
for V being LeftMod of R
for W being with_Linear_Compl Submodule of V
for L being Linear_Compl of W holds
( V is_the_direct_sum_of L,W & V is_the_direct_sum_of W,L )