let x, y, z be set ; :: thesis: ( x <> y implies <*x,y,z*> |-- y = <*z*> )
assume A1: x <> y ; :: thesis: <*x,y,z*> |-- y = <*z*>
y in {x,y,z} by ENUMSET1:def 1;
then A2: y in rng <*x,y,z*> by Lm2;
A3: y .. <*x,y,z*> = 2 by A1, Th26;
then (len <*z*>) + (y .. <*x,y,z*>) = 1 + 2 by FINSEQ_1:57
.= len <*x,y,z*> by FINSEQ_1:62 ;
then A4: len <*z*> = (len <*x,y,z*>) - (y .. <*x,y,z*>) ;

now

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:55;
then A5: k = 1 by FINSEQ_1:4, TARSKI:def 1;
hence <*z*> . k = z by FINSEQ_1:57
.= <*x,y,z*> . (k + (y .. <*x,y,z*>)) by A3, A5, FINSEQ_1:62 ;
:: thesis: verum

end;

hence <*x,y,z*> |-- y = <*z*> by A2, A4, FINSEQ_4:def 7; :: thesis: verum