let p be non-decreasing FinSequence of REAL ; :: 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

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