theorem Th7: :: PRGCOR_1:7

for i being Integer
for f being FinSequence st 1 <= i & i <= len f holds
i in dom f