let x, y be object ; :: thesis: ( x <> y iff <*x,y*> is one-to-one )
A1: <*x,y*> . 2 = y ;
2 in {1,2} by TARSKI:def 2;
then A2: 2 in dom <*x,y*> by FINSEQ_1:2, FINSEQ_1:89;
thus ( x <> y implies <*x,y*> is one-to-one ) :: thesis: ( <*x,y*> is one-to-one implies x <> y )

proof

assume A3: x <> y ; :: thesis: <*x,y*> is one-to-one
let y1, y2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not y1 in dom <*x,y*> or not y2 in dom <*x,y*> or not <*x,y*> . y1 = <*x,y*> . y2 or y1 = y2 )
assume that
A4: y1 in dom <*x,y*> and
A5: y2 in dom <*x,y*> and
A6: <*x,y*> . y1 = <*x,y*> . y2 ; :: thesis: y1 = y2
A7: y2 in {1,2} by A5, FINSEQ_1:2, FINSEQ_1:89;
A8: y1 in {1,2} by A4, FINSEQ_1:2, FINSEQ_1:89;

now :: thesis: y1 = y2

per cases ( ( y1 = 1 & y2 = 1 ) or ( y1 = 2 & y2 = 2 ) or ( y1 = 1 & y2 = 2 ) or ( y1 = 2 & y2 = 1 ) ) by A8, A7, TARSKI:def 2;

suppose ( ( y1 = 1 & y2 = 1 ) or ( y1 = 2 & y2 = 2 ) ) ; :: thesis: y1 = y2

hence y1 = y2 ; :: thesis: verum

end;

suppose A9: ( y1 = 1 & y2 = 2 ) ; :: thesis: y1 = y2

thus y1 = y2 by A3, A6, A9; :: thesis: verum

end;

suppose A10: ( y1 = 2 & y2 = 1 ) ; :: thesis: y1 = y2

thus y1 = y2 by A3, A6, A10; :: thesis: verum

end;

end;

end;

hence y1 = y2 ; :: thesis: verum

end;

assume that
A11: <*x,y*> is one-to-one and
A12: x = y ; :: thesis: contradiction
1 in {1,2} by TARSKI:def 2;
then A13: 1 in dom <*x,y*> by FINSEQ_1:2, FINSEQ_1:89;
<*x,y*> . 1 = x ;
hence contradiction by A11, A12, A13, A2, A1; :: thesis: verum