let v1, v2, v3 be object ; ( Del (<*v1*>,1) = {} & Del (<*v1,v2*>,1) = <*v2*> & Del (<*v1,v2*>,2) = <*v1*> & Del (<*v1,v2,v3*>,1) = <*v2,v3*> & Del (<*v1,v2,v3*>,2) = <*v1,v3*> & Del (<*v1,v2,v3*>,3) = <*v1,v2*> )
thus Del (<*v1*>,1) =
Del ((<*v1*> ^ {}),1)
by FINSEQ_1:34
.=
{}
by Lm14
; ( Del (<*v1,v2*>,1) = <*v2*> & Del (<*v1,v2*>,2) = <*v1*> & Del (<*v1,v2,v3*>,1) = <*v2,v3*> & Del (<*v1,v2,v3*>,2) = <*v1,v3*> & Del (<*v1,v2,v3*>,3) = <*v1,v2*> )
thus
Del (<*v1,v2*>,1) = <*v2*>
by Lm14; ( Del (<*v1,v2*>,2) = <*v1*> & Del (<*v1,v2,v3*>,1) = <*v2,v3*> & Del (<*v1,v2,v3*>,2) = <*v1,v3*> & Del (<*v1,v2,v3*>,3) = <*v1,v2*> )
len <*v1*> = 1
by FINSEQ_1:39;
hence A1: Del (<*v1,v2*>,2) =
Del ((<*v1*> ^ <*v2*>),((len <*v1*>) + 1))
.=
<*v1*>
by Lm14
;
( Del (<*v1,v2,v3*>,1) = <*v2,v3*> & Del (<*v1,v2,v3*>,2) = <*v1,v3*> & Del (<*v1,v2,v3*>,3) = <*v1,v2*> )
thus Del (<*v1,v2,v3*>,1) =
Del ((<*v1*> ^ <*v2,v3*>),1)
by FINSEQ_1:43
.=
<*v2,v3*>
by Lm14
; ( Del (<*v1,v2,v3*>,2) = <*v1,v3*> & Del (<*v1,v2,v3*>,3) = <*v1,v2*> )
A2:
len <*v1,v2*> = 2
by FINSEQ_1:44;
hence
Del (<*v1,v2,v3*>,2) = <*v1,v3*>
by A1, Lm13; Del (<*v1,v2,v3*>,3) = <*v1,v2*>
(len <*v1,v2*>) + 1 = 3
by A2;
hence
Del (<*v1,v2,v3*>,3) = <*v1,v2*>
by Lm14; verum