theorem :: TOPREALA:2

for f being FinSequence
for i being Nat holds
( not i + 1 in dom f or i in dom f or i = 0 )