for R being Ring
for V being LeftMod of R holds V is Submodule of V by VECTSP_4:24;