let C, D be non empty set ; :: thesis:
let f be one-to-one PartFunc of C,D; :: thesis:
let g be PartFunc of D,C; :: thesis:
thus ( g = f " implies ( dom g = rng f & ( for d being Element of D
for c being Element of C holds
( d in rng f & c = g /. d iff ( c in dom f & d = f /. c ) ) ) ) ) :: thesis:

proof

assume A1: g = f " ; :: thesis:
hence dom g = rng f by FUNCT_1:32; :: thesis:
let d be Element of D; :: thesis:
let c be Element of C; :: thesis:
A2: dom g = rng f by A1, FUNCT_1:32;
thus ( d in rng f & c = g /. d implies ( c in dom f & d = f /. c ) ) :: thesis:

proof

assume that
A3: d in rng f and
A4: c = g /. d ; :: thesis:
c = g . d by A2, A3, A4, PARTFUN1:def 6;
then ( c in dom f & d = f . c ) by A1, A3, FUNCT_1:32;
hence ( c in dom f & d = f /. c ) by PARTFUN1:def 6; :: thesis:

end;

assume that
A5: c in dom f and
A6: d = f /. c ; :: thesis:
d = f . c by A5, A6, PARTFUN1:def 6;
then ( d in rng f & c = g . d ) by A1, A5, FUNCT_1:32;
hence ( d in rng f & c = g /. d ) by A2, PARTFUN1:def 6; :: thesis:

end;

assume that
A7: dom g = rng f and
A8: for d being Element of D
for c being Element of C holds
( d in rng f & c = g /. d iff ( c in dom f & d = f /. c ) ) and
A9: g <> f " ; :: thesis:

now :: thesis:

per cases by A9, Th1;

suppose dom (f ") <> dom g ; :: thesis:

hence contradiction by A7, FUNCT_1:33; :: thesis:

end;

suppose ex d being Element of D st
( d in dom (f ") & (f ") /. d <> g /. d ) ; :: thesis:

then consider d being Element of D such that
A10: d in dom (f ") and
A11: (f ") /. d <> g /. d ;
(f ") /. d in rng (f ") by A10, Th2;
then A12: (f ") /. d in dom f by FUNCT_1:33;
d in rng f by A10, FUNCT_1:33;
then d = f . ((f ") . d) by FUNCT_1:35;
then d = f . ((f ") /. d) by A10, PARTFUN1:def 6;
then d = f /. ((f ") /. d) by A12, PARTFUN1:def 6;
hence contradiction by A8, A11, A12; :: thesis:

end;

end;

end;

hence contradiction ; :: thesis: