for p being FinSequence
for x being object
for n being Nat st x in rng p & n in dom (p |-- x) holds
n + (x .. p) in dom p