theorem RL5Th25: :: ZMODUL04:40

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