for i being Nat
for p being FinSequence holds
( ( i in dom p implies ex m being Nat st
( len p = m + 1 & len (Del (p,i)) = m ) ) & ( not i in dom p implies Del (p,i) = p ) )