theorem :: ZMODUL01:26

for R being Ring
for V being LeftMod of R
for W being Submodule of V holds 0. W = 0. V by VECTSP_4:def 2;