theorem Th25: :: ZMODUL01:25

for R being Ring
for V being LeftMod of R
for W being Submodule of V
for w being Vector of W holds w is Vector of V by VECTSP_4:10;