for k, m, n being Nat
for f being FinSequence st len f = m + 1 & n in dom f & n <= k & k <= m holds
(Del (f,n)) . k = f . (k + 1)