let x, y, z be set ; :: thesis: <*x,y,z*> |-- x = <*y,z*>
A1: x .. <*x,y,z*> = 1 by Th21;
then (len <*y,z*>) + (x .. <*x,y,z*>) = 2 + 1 by FINSEQ_1:44
.= len <*x,y,z*> by FINSEQ_1:45 ;
then A2: len <*y,z*> = (len <*x,y,z*>) - (x .. <*x,y,z*>) ;
A3: len <*y,z*> = 2 by FINSEQ_1:44;
A4: now :: thesis: for k being Nat st k in dom <*y,z*> holds
<*y,z*> . k = <*x,y,z*> . (k + (x .. <*x,y,z*>))
let k be Nat; :: thesis: ( k in dom <*y,z*> implies <*y,z*> . b1 = <*x,y,z*> . (b1 + (x .. <*x,y,z*>)) )
assume k in dom <*y,z*> ; :: thesis: <*y,z*> . b1 = <*x,y,z*> . (b1 + (x .. <*x,y,z*>))
then A5: k in Seg 2 by A3, FINSEQ_1:def 3;
per cases ( k = 1 or k = 2 ) by A5, FINSEQ_1:2, TARSKI:def 2;
suppose A6: k = 1 ; :: thesis: <*y,z*> . b1 = <*x,y,z*> . (b1 + (x .. <*x,y,z*>))
hence <*y,z*> . k = y by FINSEQ_1:44
.= <*x,y,z*> . (k + (x .. <*x,y,z*>)) by A1, A6, FINSEQ_1:45 ;
:: thesis: verum
end;
suppose A7: k = 2 ; :: thesis: <*y,z*> . b1 = <*x,y,z*> . (b1 + (x .. <*x,y,z*>))
hence <*y,z*> . k = z by FINSEQ_1:44
.= <*x,y,z*> . (k + (x .. <*x,y,z*>)) by A1, A7, FINSEQ_1:45 ;
:: thesis: verum
end;
end;
end;
x in {x,y,z} by ENUMSET1:def 1;
then x in rng <*x,y,z*> by Lm2;
hence <*x,y,z*> |-- x = <*y,z*> by A2, A4, FINSEQ_4:def 6; :: thesis: verum