theorem ThLin7: :: ZMODUL05:31

for V being LeftMod of INT.Ring
for A being linearly-independent Subset of V holds A is Basis of (Lin A)