let v1, v2, v3 be object ; :: 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:34
.= {} by Lm14 ; :: 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 Lm14; :: 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:39;
hence A1: Del (<*v1,v2*>,2) = Del ((<*v1*> ^ <*v2*>),((len <*v1*>) + 1))
.= <*v1*> by Lm14 ;
:: 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:43
.= <*v2,v3*> by Lm14 ; :: thesis: ( 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; :: thesis: Del (<*v1,v2,v3*>,3) = <*v1,v2*>
(len <*v1,v2*>) + 1 = 3 by A2;
hence Del (<*v1,v2,v3*>,3) = <*v1,v2*> by Lm14; :: thesis: verum