for fp being FinSequence of NAT
for n being Element of NAT
for a being Nat st len fp = n + 1 & a >= 1 & a <= n holds
(Del (fp,a)) . n = fp . (len fp)