:: deftheorem defines Del FINSEQ_3:def 2 :
for i being natural Number
for p being FinSequence holds Del (p,i) = p * (Sgm ((dom p) \ {i}));