theorem :: ZMODLAT2:17
for R being Ring
for V being LeftMod of R
for v being Vector of V
for u being object st u in Lin {v} holds
ex i being Element of R st u = i * v