theorem :: ZMODUL06:48
for X, Y being Z_Module
for T being linear-transformation of X,Y st T is bijective holds
( X is free iff Y is free )