:: deftheorem Def3 defines finite-rank ZMODUL03:def 3 :
for IT being free Z_Module holds
( IT is finite-rank iff ex A being finite Subset of IT st A is Basis of IT );