theorem HM15: :: ZMODUL06:51

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