let C, D be non empty set ; :: thesis: for f being one-to-one PartFunc of C,D
for g being PartFunc of D,C holds
( g = f " iff ( 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 ) ) ) ) )

let f be one-to-one PartFunc of C,D; :: thesis: for g being PartFunc of D,C holds
( g = f " iff ( 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 ) ) ) ) )

let g be PartFunc of D,C; :: thesis: ( g = f " iff ( 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 ) ) ) ) )

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: ( 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 ) ) ) implies g = f " )
proof
assume A1: g = f " ; :: thesis: ( 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 ) ) ) )

hence dom g = rng f by FUNCT_1:32; :: thesis: 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 ) )

let d be Element of D; :: thesis: for c being Element of C holds
( d in rng f & c = g /. d iff ( c in dom f & d = f /. c ) )

let c be Element of C; :: thesis: ( d in rng f & c = g /. d iff ( c in dom f & d = f /. c ) )
A2: dom g = rng f by ;
thus ( d in rng f & c = g /. d implies ( c in dom f & d = f /. c ) ) :: thesis: ( c in dom f & d = f /. c implies ( d in rng f & c = g /. d ) )
proof
assume that
A3: d in rng f and
A4: c = g /. d ; :: thesis: ( c in dom f & d = f /. c )
c = g . d by ;
then ( c in dom f & d = f . c ) by ;
hence ( c in dom f & d = f /. c ) by PARTFUN1:def 6; :: thesis: verum
end;
assume that
A5: c in dom f and
A6: d = f /. c ; :: thesis: ( d in rng f & c = g /. d )
d = f . c by ;
then ( d in rng f & c = g . d ) by ;
hence ( d in rng f & c = g /. d ) by ; :: thesis: verum
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: contradiction
now :: thesis: contradiction
per cases ( dom (f ") <> dom g or ex d being Element of D st
( d in dom (f ") & (f ") /. d <> g /. d ) )
by ;
suppose ex d being Element of D st
( d in dom (f ") & (f ") /. d <> g /. d ) ; :: thesis: contradiction
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 ;
then A12: (f ") /. d in dom f by FUNCT_1:33;
d in rng f by ;
then d = f . ((f ") . d) by FUNCT_1:35;
then d = f . ((f ") /. d) by ;
then d = f /. ((f ") /. d) by ;
hence contradiction by A8, A11, A12; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum