theorem Th6: :: EUCLID_7:7

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