theorem :: FUNCT_1:38

for f, g being Function st f is one-to-one & dom f = rng g & rng f = dom g & ( for x, y being object st x in dom f & y in dom g holds
( f . x = y iff g . y = x ) ) holds
g = f "