:: deftheorem defines with_Linear_Compl ZMODUL01:def 17 :
for R being Ring
for V being LeftMod of R
for W being Submodule of V holds
( W is with_Linear_Compl iff ex C being Submodule of V st V is_the_direct_sum_of C,W );