let x, y be set ; :: thesis: ( x <> y iff <*x,y*> is one-to-one )
A1: <*x,y*> . 2 = y by FINSEQ_1:44;
2 in {1,2} by TARSKI:def 2;
then A2: 2 in dom <*x,y*> by FINSEQ_1:89, FINSEQ_1:2;
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 be set ; :: according to FUNCT_1:def 4 :: thesis: for b₁ being set holds
( not y1 in proj1 <*x,y*> or not b₁ in proj1 <*x,y*> or not <*x,y*> . y1 = <*x,y*> . b₁ or y1 = b₁ )
let y2 be set ; :: thesis: ( not y1 in proj1 <*x,y*> or not y2 in proj1 <*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:89, FINSEQ_1:2;
A8: y1 in {1,2} by A4, FINSEQ_1:89, FINSEQ_1:2;

now

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

then <*x,y*> . y1 = x by FINSEQ_1:44;
hence y1 = y2 by A3, A6, A9, FINSEQ_1:44; :: thesis: verum

end;

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

then <*x,y*> . y1 = y by FINSEQ_1:44;
hence y1 = y2 by A3, A6, A10, FINSEQ_1:44; :: 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:89, FINSEQ_1:2;
<*x,y*> . 1 = x by FINSEQ_1:44;
hence contradiction by A11, A12, A13, A2, A1, FUNCT_1:def 4; :: thesis: verum