theorem :: ZMODUL01:59

for R being Ring
for V being LeftMod of R
for W being Submodule of V holds (0. V) + W = the carrier of W by VECTSP_4:45;