theorem HM1: :: ZMODUL06:42

for R being Ring
for X, Y being LeftMod of R
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 )