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 that
A1: ( f is one-to-one & dom f = rng t & rng f = dom t ) and
A2: 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 :: thesis: for x, y being object st x in dom f & y in dom t holds
( ( f . x = y implies t . y = x ) & ( t . y = x implies f . x = y ) )

let x, y be object ; :: 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 that
A3: x in dom f and
A4: y in dom t ; :: thesis: ( ( f . x = y implies t . y = x ) & ( t . y = x implies f . x = y ) )
reconsider y1 = y as Element of D by A4;
reconsider x1 = x as Element of C by A3;
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 A3, PARTFUN1:def 6;
then t /. y1 = x1 by A2, A3, A4;
hence t . y = x by A4, PARTFUN1:def 6; :: thesis: verum

end;

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

end;

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