let X, Y be set ; :: thesis: for f being Function st f is one-to-one holds
<:f,X,Y:> " = <:(f " ),Y,X:>
let f be Function; :: thesis: ( f is one-to-one implies <:f,X,Y:> " = <:(f " ),Y,X:> )
assume A1: f is one-to-one ; :: thesis: <:f,X,Y:> " = <:(f " ),Y,X:>
then A2: <:f,X,Y:> is one-to-one by Th94;
for y being set holds
( y in dom (<:f,X,Y:> " ) iff y in dom <:(f " ),Y,X:> )

proof

let y be set ; :: thesis: ( y in dom (<:f,X,Y:> " ) iff y in dom <:(f " ),Y,X:> )
thus ( y in dom (<:f,X,Y:> " ) implies y in dom <:(f " ),Y,X:> ) :: thesis: ( y in dom <:(f " ),Y,X:> implies y in dom (<:f,X,Y:> " ) )

proof

assume y in dom (<:f,X,Y:> " ) ; :: thesis: y in dom <:(f " ),Y,X:>
then A3: y in rng <:f,X,Y:> by A2, FUNCT_1:55;
then consider x being set such that
A4: x in dom <:f,X,Y:> and
A5: y = <:f,X,Y:> . x by FUNCT_1:def 5;
( dom <:f,X,Y:> c= dom f & rng <:f,X,Y:> c= rng f ) by Th77;
then ( x in dom f & y in rng f & f . x = y ) by A3, A4, A5, Th80;
then ( y in dom (f " ) & y in Y & (f " ) . y = x & x in X ) by A1, A4, Th78, FUNCT_1:54;
hence y in dom <:(f " ),Y,X:> by Th78; :: thesis: verum

end;

assume A6: y in dom <:(f " ),Y,X:> ; :: thesis: y in dom (<:f,X,Y:> " )
dom <:(f " ),Y,X:> c= dom (f " ) by Th77;
then y in dom (f " ) by A6;
then y in rng f by A1, FUNCT_1:55;
then consider x being set such that
A7: x in dom f and
A8: y = f . x by FUNCT_1:def 5;
x = (f " ) . (f . x) by A1, A7, FUNCT_1:56;
then ( x in X & f . x in Y ) by A6, A8, Th78;
then x in dom <:f,X,Y:> by A7, Th78;
then ( <:f,X,Y:> . x in rng <:f,X,Y:> & <:f,X,Y:> . x = f . x ) by Th80, FUNCT_1:def 5;
hence y in dom (<:f,X,Y:> " ) by A2, A8, FUNCT_1:55; :: thesis: verum

end;

then A9: dom (<:f,X,Y:> " ) = dom <:(f " ),Y,X:> by TARSKI:2;
for y being set st y in dom <:(f " ),Y,X:> holds
<:(f " ),Y,X:> . y = (<:f,X,Y:> " ) . y

proof

let y be set ; :: thesis: ( y in dom <:(f " ),Y,X:> implies <:(f " ),Y,X:> . y = (<:f,X,Y:> " ) . y )
assume A10: y in dom <:(f " ),Y,X:> ; :: thesis: <:(f " ),Y,X:> . y = (<:f,X,Y:> " ) . y
then ( y in rng <:f,X,Y:> & rng <:f,X,Y:> c= rng f ) by A2, A9, Th77, FUNCT_1:55;
then consider x being set such that
A11: x in dom f and
A12: y = f . x by FUNCT_1:def 5;
A13: x = (f " ) . (f . x) by A1, A11, FUNCT_1:56;
then ( x in X & f . x in Y ) by A10, A12, Th78;
then x in dom <:f,X,Y:> by A11, Th78;
then ( (<:f,X,Y:> " ) . (<:f,X,Y:> . x) = x & <:f,X,Y:> . x = f . x ) by A2, Th80, FUNCT_1:56;
hence <:(f " ),Y,X:> . y = (<:f,X,Y:> " ) . y by A10, A12, A13, Th80; :: thesis: verum

end;

hence <:f,X,Y:> " = <:(f " ),Y,X:> by A9, FUNCT_1:9; :: thesis: verum