theorem :: ZMODUL01:29

for R being Ring
for V being LeftMod of R
for v being Vector of V
for a being Element of R
for W being Submodule of V
for w being Vector of W st w = v holds
a * w = a * v by VECTSP_4:14;