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