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

now

let x, y be set ; :: thesis: ( x in dom f & y in dom t implies ( ( f . x = y implies t . y = x ) & ( t . y = x implies f . x = y ) ) )
assume A2: ( x in dom f & y in dom t ) ; :: thesis: ( ( f . x = y implies t . y = x ) & ( t . y = x implies f . x = y ) )
then reconsider x1 = x as Element of C ;
reconsider y1 = y as Element of D by A2;
thus ( f . x = y implies t . y = x ) :: thesis: ( t . y = x implies f . x = y )

proof

assume f . x = y ; :: thesis: t . y = x
then f /. x1 = y1 by A2, PARTFUN1:def 8;
then t /. y1 = x1 by A1, A2;
hence t . y = x by A2, PARTFUN1:def 8; :: thesis: verum

end;

assume t . y = x ; :: thesis: f . x = y
then t /. y1 = x1 by A2, PARTFUN1:def 8;
then f /. x1 = y1 by A1, A2;
hence f . x = y by A2, PARTFUN1:def 8; :: thesis: verum

end;

hence t = f " by A1, FUNCT_1:60; :: thesis: verum