theorem Th6: :: PENCIL_2:6

for D being set
for p being FinSequence of D
for i, j, k being Element of NAT st i in dom p & j in dom p & i <= j & i <= k & k <= (((len p) - j) + i) - 1 holds
(Del (p,i,j)) . k = p . (((j -' i) + k) + 1)