theorem Th17: :: RFINSEQ2:17

for R being FinSequence of REAL holds
( R is non-decreasing iff for n, m being Nat st n in dom R & m in dom R & n < m holds
R . n <= R . m )