for R being Ring
for V being RightMod of R
for W being Submodule of V holds 0. W = 0. V by Def2;