theorem :: ZMODUL06:50

for X, Y being free Z_Module
for T being linear-transformation of X,Y st T is bijective holds
( X is finite-rank iff Y is finite-rank )