theorem :: ZMODUL04:20

for V being free Z_Module
for I, A being Subset of V st I is Basis of V & I is finite & A is linearly-independent holds
card A c= card I by XXTh3, XBOOLE_0:def 8;