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;

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

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*>))

x in {x,y,z}
by ENUMSET1:def 1;<*y,z*> . k = <*x,y,z*> . (k + (x .. <*x,y,z*>))

let k be Nat; :: thesis: ( k in dom <*y,z*> implies <*y,z*> . b_{1} = <*x,y,z*> . (b_{1} + (x .. <*x,y,z*>)) )

assume k in dom <*y,z*> ; :: thesis: <*y,z*> . b_{1} = <*x,y,z*> . (b_{1} + (x .. <*x,y,z*>))

then A5: k in Seg 2 by A3, FINSEQ_1:def 3;

end;assume k in dom <*y,z*> ; :: thesis: <*y,z*> . b

then A5: k in Seg 2 by A3, FINSEQ_1:def 3;

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