let X, Y be free finite-rank Z_Module; :: thesis: for T being linear-transformation of X,Y st T is bijective holds
rank X = rank Y
let T be linear-transformation of X,Y; :: thesis: ( T is bijective implies rank X = rank Y )
assume AS1: T is bijective ; :: thesis: rank X = rank Y
for I being Basis of X holds rank Y = card I

proof

let I be Basis of X; :: thesis: rank Y = card I
dom T = the carrier of X by FUNCT_2:def 1;
then X12: card I = card (T .: I) by CARD_1:5, AS1, CARD_1:33;
T .: I is Basis of Y by AS1, HM12;
hence rank Y = card I by X12, ZMODUL03:def 5; :: thesis: verum

end;

hence rank X = rank Y by ZMODUL03:def 5; :: thesis: verum