let X, Y be free Z_Module; :: thesis: for T being linear-transformation of X,Y st T is bijective holds
( X is finite-rank iff Y is finite-rank )
let T be linear-transformation of X,Y; :: thesis: ( T is bijective implies ( X is finite-rank iff Y is finite-rank ) )
assume AS1: T is bijective ; :: thesis: ( X is finite-rank iff Y is finite-rank )
consider K being linear-transformation of Y,X such that
AS3: ( K = T " & K is bijective ) by HM1, AS1;
thus ( X is finite-rank iff Y is finite-rank ) by HM13, AS1, AS3; :: thesis: verum