theorem Th107: :: FINSEQ_3:109

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