let v1, v2, v3 be set ; :: thesis: ( 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 Lm16 ; :: thesis: ( 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 Lm16; :: thesis: ( 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 Lm16 ;
:: thesis: ( 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 Lm16 ; :: thesis: ( Del <*v1,v2,v3*>,2 = <*v1,v3*> & Del <*v1,v2,v3*>,3 = <*v1,v2*> )
A2: len <*v1,v2*> = 2 by FINSEQ_1:61;
then A3: ( 2 <= len <*v1,v2*> & (len <*v1,v2*>) + 1 = 3 ) ;
thus Del <*v1,v2,v3*>,2 = <*v1,v3*> by A1, A2, Lm15; :: thesis: Del <*v1,v2,v3*>,3 = <*v1,v2*>
thus Del <*v1,v2,v3*>,3 = <*v1,v2*> by A3, Lm16; :: thesis: verum