for R being Ring
for V being LeftMod of R
for v being Vector of V
for i being Element of R holds i * v in Lin {v} by ThLin2, VECTSP_4:21;