theorem Th30: :: INT_4:30

for fp being FinSequence of NAT
for d, b, n being Element of NAT st b in dom fp & len fp = n + 1 holds
Del ((fp ^ <*d*>),b) = (Del (fp,b)) ^ <*d*>