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 "

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 ) )

hence
t = f "
by A1, FUNCT_1:38; :: thesis: verum( ( 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 )

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;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
t . y = x
; :: thesis: f . x = y
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;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

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