for R being Ring
for V being LeftMod of R
for v1, v2 being Vector of V st R is commutative & not R is degenerated & {v1,v2} is linearly-independent holds
v1 <> 0. V by VECTSP_7:4;