let V be free finite-rank Z_Module; :: thesis: for b being OrdBasis of V holds len b = rank V
let b be OrdBasis of V; :: thesis: len b = rank V
reconsider R = rng b as Basis of V by defOrdBasis;
A1: b is one-to-one by defOrdBasis;
thus len b = card (Seg (len b)) by FINSEQ_1:57
.= card (dom b) by FINSEQ_1:def 3
.= card R by A1, CARD_1:70
.= rank V by ZMODUL03:def 5 ; :: thesis: verum