let x, y be set ; :: thesis: <*x,y*> |-- x = <*y*>
A1: x .. <*x,y*> = 1 by Th19;
then (len <*y*>) + (x .. <*x,y*>) = 1 + 1 by FINSEQ_1:40
.= len <*x,y*> by FINSEQ_1:44 ;
then A2: len <*y*> = (len <*x,y*>) - (x .. <*x,y*>) ;

A3: now :: thesis: for k being Nat st k in dom <*y*> holds
<*y*> . k = <*x,y*> . (k + (x .. <*x,y*>))

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:38;
then A4: k = 1 by FINSEQ_1:2, TARSKI:def 1;
hence <*y*> . k = y
.= <*x,y*> . (k + (x .. <*x,y*>)) by A1, A4 ;
:: thesis: verum

end;

x in {x,y} by TARSKI:def 2;
then x in rng <*x,y*> by Lm1;
hence <*x,y*> |-- x = <*y*> by A2, A3, FINSEQ_4:def 6; :: thesis: verum