let x, y, z be set ; <*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 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;
( k in dom <*y,z*> implies <*y,z*> . b1 = <*x,y,z*> . (b1 + (x .. <*x,y,z*>)) )assume
k in dom <*y,z*>
;
<*y,z*> . b1 = <*x,y,z*> . (b1 + (x .. <*x,y,z*>))then A5:
k in Seg 2
by A3, FINSEQ_1:def 3;
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; verum