let i be natural number ; :: 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 set 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) by TARSKI:def 3;
then rng (Sgm ((Seg (len p)) \ {i})) c= Seg (len p) by FINSEQ_1:def 13;
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:35; :: 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 Th113; :: thesis: verum

end;

end;