for R being Ring
for V being LeftMod of R
for A being Subset of V st not R is degenerated & A is linearly-independent holds
not 0. V in A by VECTSP_7:2;