let x, y, z be set ; :: thesis: ( x <> y implies <*x,y,z*> |-- y = <*z*> )
assume x <> y ; :: thesis: <*x,y,z*> |-- y = <*z*>
then A1: y .. <*x,y,z*> = 2 by Th22;
then (len <*z*>) + (y .. <*x,y,z*>) = 1 + 2 by FINSEQ_1:40
.= len <*x,y,z*> by FINSEQ_1:45 ;
then A2: len <*z*> = (len <*x,y,z*>) - (y .. <*x,y,z*>) ;

A3: now :: thesis: for k being Nat st k in dom <*z*> holds
<*z*> . k = <*x,y,z*> . (k + (y .. <*x,y,z*>))

let k be Nat; :: thesis: ( k in dom <*z*> implies <*z*> . k = <*x,y,z*> . (k + (y .. <*x,y,z*>)) )
assume k in dom <*z*> ; :: thesis: <*z*> . k = <*x,y,z*> . (k + (y .. <*x,y,z*>))
then k in Seg 1 by FINSEQ_1:38;
then A4: k = 1 by FINSEQ_1:2, TARSKI:def 1;
hence <*z*> . k = z
.= <*x,y,z*> . (k + (y .. <*x,y,z*>)) by A1, A4 ;
:: thesis: verum

end;

y in {x,y,z} by ENUMSET1:def 1;
then y in rng <*x,y,z*> by Lm2;
hence <*x,y,z*> |-- y = <*z*> by A2, A3, FINSEQ_4:def 6; :: thesis: verum