theorem Th25: :: FINSEQ_3:25

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