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;
A6: f . x = y by A4, A5, Th80;
then A7: y in Y by A4, Th78;
rng <:f,X,Y:> c= rng f by Th77;
then y in rng f by A3;
then A8: y in dom (f " ) by A1, FUNCT_1:54;
dom <:f,X,Y:> c= dom f by Th77;
then (f " ) . y = x by A1, A4, A6, FUNCT_1:54;
hence y in dom <:(f " ),Y,X:> by A4, A8, A7, Th78; :: thesis: verum

end;

assume A9: 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 A9;
then y in rng f by A1, FUNCT_1:55;
then consider x being set such that
A10: x in dom f and
A11: y = f . x by FUNCT_1:def 5;
x = (f " ) . (f . x) by A1, A10, FUNCT_1:56;
then x in X by A9, A11, Th78;
then x in dom <:f,X,Y:> by A9, A10, A11, 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, A11, FUNCT_1:55; :: thesis: verum

end;

then A12: 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 )
A13: rng <:f,X,Y:> c= rng f by Th77;
assume A14: y in dom <:(f " ),Y,X:> ; :: thesis: <:(f " ),Y,X:> . y = (<:f,X,Y:> " ) . y
then y in rng <:f,X,Y:> by A2, A12, FUNCT_1:55;
then consider x being set such that
A15: x in dom f and
A16: y = f . x by A13, FUNCT_1:def 5;
A17: x = (f " ) . (f . x) by A1, A15, FUNCT_1:56;
then x in X by A14, A16, Th78;
then x in dom <:f,X,Y:> by A14, A15, A16, 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 A14, A16, A17, Th80; :: thesis: verum

end;

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