theorem LmRankSX1: :: ZMODUL07:6

for V being free finite-rank Z_Module
for A being linearly-independent Subset of V ex I being finite linearly-independent Subset of V st
( A c= I & rank V = card I )