let p be real-valued non-decreasing FinSequence; :: thesis: for i, j being Nat st i in dom p & j in dom p & i <= j holds
p . i <= p . j
for n being Nat st n in dom p & n + 1 in dom p holds
p . n <= p . (n + 1) by Def1;
hence for i, j being Nat st i in dom p & j in dom p & i <= j holds
p . i <= p . j by LM; :: thesis: verum