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

now

let k be Nat; :: thesis: ( k in dom <*y,z*> implies <*y,z*> . b₁ = <*x,y,z*> . (b₁ + (x .. <*x,y,z*>)) )
assume k in dom <*y,z*> ; :: thesis: <*y,z*> . b₁ = <*x,y,z*> . (b₁ + (x .. <*x,y,z*>))
then A5: k in Seg 2 by A4, FINSEQ_1:def 3;

per cases ( k = 1 or k = 2 ) by A5, FINSEQ_1:4, TARSKI:def 2;

suppose A6: k = 1 ; :: thesis: <*y,z*> . b₁ = <*x,y,z*> . (b₁ + (x .. <*x,y,z*>))

hence <*y,z*> . k = y by FINSEQ_1:61
.= <*x,y,z*> . (k + (x .. <*x,y,z*>)) by A2, A6, FINSEQ_1:62 ;
:: thesis: verum

end;

suppose A7: k = 2 ; :: thesis: <*y,z*> . b₁ = <*x,y,z*> . (b₁ + (x .. <*x,y,z*>))

hence <*y,z*> . k = z by FINSEQ_1:61
.= <*x,y,z*> . (k + (x .. <*x,y,z*>)) by A2, A7, FINSEQ_1:62 ;
:: thesis: verum

end;

end;

end;

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