let x, y be set ; :: thesis: ( x <> y iff <*x,y*> is one-to-one )
thus ( x <> y implies <*x,y*> is one-to-one ) :: thesis: ( <*x,y*> is one-to-one implies x <> y )

proof

assume A1: x <> y ; :: thesis: <*x,y*> is one-to-one
let y1 be set ; :: according to FUNCT_1:def 8 :: thesis: for b₁ being set holds
( not y1 in dom <*x,y*> or not b₁ in dom <*x,y*> or not <*x,y*> . y1 = <*x,y*> . b₁ or y1 = b₁ )
let y2 be set ; :: 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
A2: ( y1 in dom <*x,y*> & y2 in dom <*x,y*> ) and
A3: <*x,y*> . y1 = <*x,y*> . y2 ; :: thesis: y1 = y2
A4: ( y1 in {1,2} & y2 in {1,2} ) by A2, Th29, FINSEQ_1:4;

now

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

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

hence y1 = y2 ; :: thesis: verum

end;

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

then ( <*x,y*> . y1 = x & <*x,y*> . y2 = y ) by FINSEQ_1:61;
hence y1 = y2 by A1, A3; :: thesis: verum

end;

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

then ( <*x,y*> . y1 = y & <*x,y*> . y2 = x ) by FINSEQ_1:61;
hence y1 = y2 by A1, A3; :: thesis: verum

end;

end;

end;

hence y1 = y2 ; :: thesis: verum

end;

assume A5: ( <*x,y*> is one-to-one & x = y ) ; :: thesis: contradiction
( 1 in {1,2} & 2 in {1,2} ) by TARSKI:def 2;
then ( 1 in dom <*x,y*> & 2 in dom <*x,y*> & 1 <> 2 & <*x,y*> . 1 = x & <*x,y*> . 2 = y ) by Th29, FINSEQ_1:4, FINSEQ_1:61;
hence contradiction by A5, FUNCT_1:def 8; :: thesis: verum