for K being Ring
for V being LeftMod of K
for A being Subset of V st not K is trivial & A is linearly-independent holds
not 0. V in A