let v1, v2, v3 be set ; ( 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:47
.=
{}
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:56;
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:60
.=
<*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:61;
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