for n, k being Nat
for f being FinSequence of REAL st k in dom (f /^ n) & n in dom f holds
n + k in dom f