let a, b, c, d be set ; :: thesis: not ( ( a = b implies c = d ) & ( c = d implies a = b ) & not (a,b --> c,d) " = c,d --> a,b )
assume A1: ( a = b iff c = d ) ; :: thesis: (a,b --> c,d) " = c,d --> a,b

per cases ( ( a = b & c = d ) or ( a <> b & c <> d ) ) by A1;

suppose A2: ( a = b & c = d ) ; :: thesis: (a,b --> c,d) " = c,d --> a,b

(a,a --> d,d) " = (a .--> d) " by FUNCT_4:86
.= d .--> a by Th10
.= d,d --> a,a by FUNCT_4:86 ;
hence (a,b --> c,d) " = c,d --> a,b by A2; :: thesis: verum

end;

suppose A3: ( a <> b & c <> d ) ; :: thesis: (a,b --> c,d) " = c,d --> a,b

set f = a,b --> c,d;
set g = c,d --> a,b;
A4: for y, x being set holds
( y in rng (a,b --> c,d) & x = (c,d --> a,b) . y iff ( x in dom (a,b --> c,d) & y = (a,b --> c,d) . x ) )

proof

let y, x be set ; :: thesis: ( y in rng (a,b --> c,d) & x = (c,d --> a,b) . y iff ( x in dom (a,b --> c,d) & y = (a,b --> c,d) . x ) )
A5: ( x in dom (a,b --> c,d) & y = (a,b --> c,d) . x implies ( y in rng (a,b --> c,d) & x = (c,d --> a,b) . y ) )

proof

assume that
A6: x in dom (a,b --> c,d) and
A7: y = (a,b --> c,d) . x ; :: thesis: ( y in rng (a,b --> c,d) & x = (c,d --> a,b) . y )
A8: x in {a,b} by A6, FUNCT_4:65;

per cases ( x = a or x = b ) by A8, TARSKI:def 2;

suppose A9: x = a ; :: thesis: ( y in rng (a,b --> c,d) & x = (c,d --> a,b) . y )

then A10: y = c by A3, A7, FUNCT_4:66;
then y in {c,d} by TARSKI:def 2;
hence ( y in rng (a,b --> c,d) & x = (c,d --> a,b) . y ) by A3, A9, A10, FUNCT_4:66, FUNCT_4:67; :: thesis: verum

end;

suppose A11: x = b ; :: thesis: ( y in rng (a,b --> c,d) & x = (c,d --> a,b) . y )

then A12: y = d by A7, FUNCT_4:66;
then y in {c,d} by TARSKI:def 2;
hence ( y in rng (a,b --> c,d) & x = (c,d --> a,b) . y ) by A3, A11, A12, FUNCT_4:66, FUNCT_4:67; :: thesis: verum

end;

end;

end;

( y in rng (a,b --> c,d) & x = (c,d --> a,b) . y implies ( x in dom (a,b --> c,d) & y = (a,b --> c,d) . x ) )

proof

assume that
A13: y in rng (a,b --> c,d) and
A14: x = (c,d --> a,b) . y ; :: thesis: ( x in dom (a,b --> c,d) & y = (a,b --> c,d) . x )
A15: y in {c,d} by A3, A13, FUNCT_4:67;

per cases ( y = c or y = d ) by A15, TARSKI:def 2;

suppose A16: y = c ; :: thesis: ( x in dom (a,b --> c,d) & y = (a,b --> c,d) . x )

then A17: x = a by A3, A14, FUNCT_4:66;
then x in {a,b} by TARSKI:def 2;
hence ( x in dom (a,b --> c,d) & y = (a,b --> c,d) . x ) by A3, A16, A17, FUNCT_4:65, FUNCT_4:66; :: thesis: verum

end;

suppose A18: y = d ; :: thesis: ( x in dom (a,b --> c,d) & y = (a,b --> c,d) . x )

then A19: x = b by A14, FUNCT_4:66;
then x in {a,b} by TARSKI:def 2;
hence ( x in dom (a,b --> c,d) & y = (a,b --> c,d) . x ) by A18, A19, FUNCT_4:65, FUNCT_4:66; :: thesis: verum

end;

end;

end;

hence ( y in rng (a,b --> c,d) & x = (c,d --> a,b) . y iff ( x in dom (a,b --> c,d) & y = (a,b --> c,d) . x ) ) by A5; :: thesis: verum

end;

A20: a,b --> c,d is one-to-one

proof

A21: dom (a,b --> c,d) = {a,b} by FUNCT_4:65;
let x1, x2 be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x1 in proj1 (a,b --> c,d) or not x2 in proj1 (a,b --> c,d) or not (a,b --> c,d) . x1 = (a,b --> c,d) . x2 or x1 = x2 )
assume that
A22: ( x1 in dom (a,b --> c,d) & x2 in dom (a,b --> c,d) ) and
A23: (a,b --> c,d) . x1 = (a,b --> c,d) . x2 ; :: thesis: x1 = x2

per cases ( ( x1 = a & x2 = a ) or ( x1 = b & x2 = b ) or ( x1 = a & x2 = b ) or ( x1 = b & x2 = a ) ) by A22, A21, TARSKI:def 2;

suppose ( ( x1 = a & x2 = a ) or ( x1 = b & x2 = b ) ) ; :: thesis: x1 = x2

hence x1 = x2 ; :: thesis: verum

end;

suppose A24: ( x1 = a & x2 = b ) ; :: thesis: x1 = x2

then (a,b --> c,d) . x1 = c by A3, FUNCT_4:66;
hence x1 = x2 by A3, A23, A24, FUNCT_4:66; :: thesis: verum

end;

suppose A25: ( x1 = b & x2 = a ) ; :: thesis: x1 = x2

then (a,b --> c,d) . x1 = d by FUNCT_4:66;
hence x1 = x2 by A3, A23, A25, FUNCT_4:66; :: thesis: verum

end;

end;

end;

dom (c,d --> a,b) = {c,d} by FUNCT_4:65
.= rng (a,b --> c,d) by A3, FUNCT_4:67 ;
hence (a,b --> c,d) " = c,d --> a,b by A20, A4, FUNCT_1:54; :: thesis: verum

end;

end;