theorem HM12: :: ZMODUL06:49

for X, Y being free Z_Module
for T being linear-transformation of X,Y
for A being Subset of X st T is bijective holds
( A is Basis of X iff T .: A is Basis of Y )