theorem Th124: :: ZMODUL01:124

for V being Z_Module
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 )