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

then x in rng <*x,y*> by Lm1;

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

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

x in {x,y}
by TARSKI:def 2;<*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 by FINSEQ_1:40

.= <*x,y*> . (k + (x .. <*x,y*>)) by A1, A4, FINSEQ_1:44 ;

:: thesis: verum

end;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 by FINSEQ_1:40

.= <*x,y*> . (k + (x .. <*x,y*>)) by A1, A4, FINSEQ_1:44 ;

:: thesis: verum

then x in rng <*x,y*> by Lm1;

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