theorem Th1: :: MSUALG_8:1

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