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