theorem Th4: :: PENCIL_2:4

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