theorem :: SEQ_4:137

for v being FinSequence of REAL st v is increasing holds
for n, m being Nat st n in dom v & m in dom v & n <= m holds
v . n <= v . m