:: deftheorem Def5 defines rank ZMODUL03:def 5 :
for V being free finite-rank Z_Module
for b₂ being Nat holds
( b₂ = rank V iff for I being Basis of V holds b₂ = card I );