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 Th37;
for y being object holds
( y in dom (<:f,X,Y:> ") iff y in dom <:(f "),Y,X:> )

proof

let y be object ; :: 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:33;
then consider x being object such that
A4: x in dom <:f,X,Y:> and
A5: y = <:f,X,Y:> . x by FUNCT_1:def 3;
A6: f . x = y by A4, A5, Th26;
then A7: y in Y by A4, Th24;
rng <:f,X,Y:> c= rng f by Th23;
then y in rng f by A3;
then A8: y in dom (f ") by A1, FUNCT_1:32;
dom <:f,X,Y:> c= dom f by Th23;
then (f ") . y = x by A1, A4, A6, FUNCT_1:32;
hence y in dom <:(f "),Y,X:> by A4, A8, A7, Th24; :: 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 Th23;
then y in dom (f ") by A9;
then y in rng f by A1, FUNCT_1:33;
then consider x being object such that
A10: x in dom f and
A11: y = f . x by FUNCT_1:def 3;
x = (f ") . (f . x) by A1, A10, FUNCT_1:34;
then x in X by A9, A11, Th24;
then x in dom <:f,X,Y:> by A9, A10, A11, Th24;
then ( <:f,X,Y:> . x in rng <:f,X,Y:> & <:f,X,Y:> . x = f . x ) by Th26, FUNCT_1:def 3;
hence y in dom (<:f,X,Y:> ") by A2, A11, FUNCT_1:33; :: thesis: verum

end;

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

proof

let y be object ; :: 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 Th23;
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:33;
then consider x being object such that
A15: x in dom f and
A16: y = f . x by A13, FUNCT_1:def 3;
A17: x = (f ") . (f . x) by A1, A15, FUNCT_1:34;
then x in X by A14, A16, Th24;
then x in dom <:f,X,Y:> by A14, A15, A16, Th24;
then ( (<:f,X,Y:> ") . (<:f,X,Y:> . x) = x & <:f,X,Y:> . x = f . x ) by A2, Th26, FUNCT_1:34;
hence <:(f "),Y,X:> . y = (<:f,X,Y:> ") . y by A14, A16, A17, Th26; :: thesis: verum

end;

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