theorem Th1: :: LMOD_7:1

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