theorem Th2: :: PROB_3:2

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