theorem :: ZMODUL01:47

for R being Ring
for V being strict LeftMod of R
for W being strict Submodule of V st the carrier of W = the carrier of V holds
W = V by VECTSP_4:31;