for n being Nat
for f being FinSequence of REAL holds
( n + 1 <= len f iff n + 1 in dom f )