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 A1: i in dom p ; :: thesis: Del p,i is FinSequence of D

(Seg (len p)) \ {i} c= Seg (len p)

proof

for x being set st x in (Seg (len p)) \ {i} holds
x in Seg (len p) by XBOOLE_0:def 5;
hence (Seg (len p)) \ {i} c= Seg (len p) by TARSKI:def 3; :: thesis: verum

end;

then A2: rng (Sgm ((Seg (len p)) \ {i})) c= Seg (len p) by FINSEQ_1:def 13;
reconsider D' = Seg (len p) as non empty set by A1, FINSEQ_1:def 3;
reconsider q = Sgm ((Seg (len p)) \ {i}) as FinSequence of D' by A2, 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;