for R being Ring
for V being RightMod of R
for W being Submodule of V
for w being Vector of W holds w is Vector of V