let x, y, z be set ; :: thesis: ( ( x <> y & y <> z & z <> x ) iff <*x,y,z*> is one-to-one )
set p = <*x,y,z*>;
A1: <*x,y,z*> . 1 = x by FINSEQ_1:62;
A2: <*x,y,z*> . 3 = z by FINSEQ_1:62;
thus ( x <> y & y <> z & z <> x implies <*x,y,z*> is one-to-one ) :: thesis: ( <*x,y,z*> is one-to-one implies ( x <> y & y <> z & z <> x ) )

proof

assume that
A3: x <> y and
A4: y <> z and
A5: z <> x ; :: thesis: <*x,y,z*> is one-to-one
{x,y} /\ {z} = {}

proof

consider y1 being Element of {x,y} /\ {z};
assume A6: not {x,y} /\ {z} = {} ; :: thesis: contradiction
then y1 in {x,y} by XBOOLE_0:def 4;
then A7: ( y1 = x or y1 = y ) by TARSKI:def 2;
y1 in {z} by A6, XBOOLE_0:def 4;
hence contradiction by A4, A5, A7, TARSKI:def 1; :: thesis: verum

end;

then {} = (rng <*x,y*>) /\ {z} by FINSEQ_2:147
.= (rng <*x,y*>) /\ (rng <*z*>) by FINSEQ_1:55 ;
then A8: rng <*x,y*> misses rng <*z*> by XBOOLE_0:def 7;
A9: <*z*> is one-to-one by Th102;
<*x,y*> is one-to-one by A3, Th103;
then <*x,y*> ^ <*z*> is one-to-one by A8, A9, Th98;
hence <*x,y,z*> is one-to-one by FINSEQ_1:60; :: thesis: verum

end;

A10: <*x,y,z*> . 2 = y by FINSEQ_1:62;
1 in {1,2,3} by ENUMSET1:def 1;
then A11: 1 in dom <*x,y,z*> by Th1, Th30;
3 in {1,2,3} by ENUMSET1:def 1;
then A12: 3 in dom <*x,y,z*> by Th1, Th30;
2 in {1,2,3} by ENUMSET1:def 1;
then A13: 2 in dom <*x,y,z*> by Th1, Th30;
assume <*x,y,z*> is one-to-one ; :: thesis: ( x <> y & y <> z & z <> x )
hence ( x <> y & y <> z & z <> x ) by A11, A13, A12, A1, A10, A2, FUNCT_1:def 8; :: thesis: verum