theorem LmTF1D: :: ZMODUL07:4

for V being free finite-rank Z_Module
for I being linearly-independent Subset of V holds I is finite