theorem HM1: :: ZMODUL06:42

for X, Y being Z_Module
for L being linear-transformation of X,Y st L is bijective holds
ex K being linear-transformation of Y,X st
( K = L " & K is bijective )