let i be Nat; :: thesis: for D being non empty set
for p being FinSequence of D holds Del (p,i) is FinSequence of D
let D be non empty set ; :: thesis: for p being FinSequence of D holds Del (p,i) is FinSequence of D
let p be FinSequence of D; :: thesis: Del (p,i) is FinSequence of D

per cases ( i in dom p or not i in dom p ) ;

suppose i in dom p ; :: thesis: Del (p,i) is FinSequence of D

then reconsider D9 = Seg (len p) as non empty set by FINSEQ_1:def 3;
for x being object st x in (Seg (len p)) \ {i} holds
x in Seg (len p) by XBOOLE_0:def 5;
then (Seg (len p)) \ {i} c= Seg (len p) ;
then rng (Sgm ((Seg (len p)) \ {i})) c= Seg (len p) by FINSEQ_1:def 14;
then reconsider q = Sgm ((Seg (len p)) \ {i}) as FinSequence of D9 by FINSEQ_1:def 4;
p * q = Del (p,i) by FINSEQ_1:def 3;
hence Del (p,i) is FinSequence of D by FINSEQ_2:31; :: thesis: verum

end;

suppose not i in dom p ; :: thesis: Del (p,i) is FinSequence of D

hence Del (p,i) is FinSequence of D by Th102; :: thesis: verum

end;

end;