for i, n being Nat
for f being FinSequence st i in dom (f /^ n) holds
n + i in dom f