theorem :: SEQ_4:134

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