theorem Th7: :: EUCLID_7:8

for h being natural-valued FinSequence st h is increasing holds
for i being Nat st i <= len h & 1 <= h . 1 holds
i <= h . i