for R being Ring
for V being LeftMod of R
for v being Vector of V holds v in Lin {v} by VECTSP_7:8, ZFMISC_1:31;