let X, Y be free Z_Module; :: thesis: for T being linear-transformation of X,Y st T is bijective & X is finite-rank holds
Y is finite-rank
let L be linear-transformation of X,Y; :: thesis: ( L is bijective & X is finite-rank implies Y is finite-rank )
assume AS1: L is bijective ; :: thesis: ( not X is finite-rank or Y is finite-rank )
assume X is finite-rank ; :: thesis: Y is finite-rank
then consider A being finite Subset of X such that
P1: A is Basis of X ;
L .: A is Basis of Y by P1, HM12, AS1;
hence Y is finite-rank ; :: thesis: verum