for p being non-decreasing FinSequence of REAL
for i, j being Nat st i in dom p & j in dom p & i <= j holds
p . i <= p . j