theorem :: ZMODUL01:125

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 W + L = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #)