let f, g be Function; :: thesis: ( 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 ) ) implies g = f " )
assume that
A1: f is one-to-one and
A2: dom f = rng g and
A3: rng f = dom g and
A4: for x, y being object st x in dom f & y in dom g holds
( f . x = y iff g . y = x ) ; :: thesis: g = f "
A5: for y being object st y in dom g holds
g . y = (f ") . y

proof

let y be object ; :: thesis: ( y in dom g implies g . y = (f ") . y )
assume A6: y in dom g ; :: thesis: g . y = (f ") . y
then A7: g . y in dom f by A2, Def3;
then f . (g . y) = y by A4, A6;
hence g . y = (f ") . y by A1, A7, Th31; :: thesis: verum

end;

rng f = dom (f ") by A1, Th31;
hence g = f " by A3, A5, Th2; :: thesis: verum