let x, y be set ; :: thesis: <*x,y*> |-- x = <*y*>
x in {x,y} by TARSKI:def 2;
then A1: x in rng <*x,y*> by Lm1;
A2: x .. <*x,y*> = 1 by Th23;
then (len <*y*>) + (x .. <*x,y*>) = 1 + 1 by FINSEQ_1:57
.= len <*x,y*> by FINSEQ_1:61 ;
then A3: len <*y*> = (len <*x,y*>) - (x .. <*x,y*>) ;

now

let k be Nat; :: thesis: ( k in dom <*y*> implies <*y*> . k = <*x,y*> . (k + (x .. <*x,y*>)) )
assume k in dom <*y*> ; :: thesis: <*y*> . k = <*x,y*> . (k + (x .. <*x,y*>))
then k in Seg 1 by FINSEQ_1:55;
then A4: k = 1 by FINSEQ_1:4, TARSKI:def 1;
hence <*y*> . k = y by FINSEQ_1:57
.= <*x,y*> . (k + (x .. <*x,y*>)) by A2, A4, FINSEQ_1:61 ;
:: thesis: verum

end;

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