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:

assume A1: g = f " ; :: thesis:
then A2: ( dom g = rng f & ( for y, x being set holds
( y in rng f & x = g . y iff ( x in dom f & y = f . x ) ) ) ) by FUNCT_1:54;
thus dom g = rng f by A1, FUNCT_1:54; :: thesis:
let d be Element of D; :: thesis:
let c be Element of C; :: thesis:
thus ( d in rng f & c = g /. d implies ( c in dom f & d = f /. c ) ) :: thesis:

assume A3: ( d in rng f & c = g /. d ) ; :: thesis:
then c = g . d by A2, PARTFUN1:def 8;
then ( c in dom f & d = f . c ) by A1, A3, FUNCT_1:54;
hence ( c in dom f & d = f /. c ) by PARTFUN1:def 8; :: thesis:

end;

assume ( c in dom f & d = f /. c ) ; :: thesis:
then ( c in dom f & d = f . c ) by PARTFUN1:def 8;
then ( d in rng f & c = g . d ) by A1, FUNCT_1:54;
hence ( d in rng f & c = g /. d ) by A2, PARTFUN1:def 8; :: thesis:

end;

assume that
A4: dom g = rng f and
A5: 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
A6: g <> f " ; :: thesis:

per cases by A6, Th3;

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

hence contradiction by A4, FUNCT_1:55; :: 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
A7: ( d in dom (f " ) & (f " ) /. d <> g /. d ) ;
A8: d in rng f by A7, FUNCT_1:55;
(f " ) /. d in rng (f " ) by A7, Th4;
then A9: (f " ) /. d in dom f by FUNCT_1:55;
d = f . ((f " ) . d) by A8, FUNCT_1:57;
then d = f . ((f " ) /. d) by A7, PARTFUN1:def 8;
then d = f /. ((f " ) /. d) by A9, PARTFUN1:def 8;
hence contradiction by A5, A7, A9; :: thesis:

end;

hence contradiction ; :: thesis: