theorem :: SEQM_3:44

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