theorem ThLin7: :: ZMODUL05:31

for V being Z_Module
for A being linearly-independent Subset of V holds A is Basis of (Lin A)