let R be real-valued FinSequence; :: thesis: ( ( len R = 0 or len R = 1 ) implies R is non-decreasing FinSequence of REAL )
assume A1: ( len R = 0 or len R = 1 ) ; :: thesis: R is non-decreasing FinSequence of REAL
reconsider R = R as FinSequence of REAL by RVSUM_1:145;

per cases ( len R = 0 or len R = 1 ) by A1;

suppose len R = 0 ; :: thesis: R is non-decreasing FinSequence of REAL

then R = <*> REAL ;
then for n being Nat st n in dom R & n + 1 in dom R holds
R . n <= R . (n + 1) ;
hence R is non-decreasing FinSequence of REAL by INTEGRA2:def 1; :: thesis: verum

end;

suppose len R = 1 ; :: thesis: R is non-decreasing FinSequence of REAL

then A2: dom R = {1} by FINSEQ_1:2, FINSEQ_1:def 3;

now :: thesis: for n being Nat st n in dom R & n + 1 in dom R holds
R . n <= R . (n + 1)

let n be Nat; :: thesis: ( n in dom R & n + 1 in dom R implies R . n <= R . (n + 1) )
assume that
A3: n in dom R and
A4: n + 1 in dom R ; :: thesis: R . n <= R . (n + 1)
n = 1 by A2, A3, TARSKI:def 1;
hence R . n <= R . (n + 1) by A2, A4, TARSKI:def 1; :: thesis: verum

end;

hence R is non-decreasing FinSequence of REAL by INTEGRA2:def 1; :: thesis: verum

end;

end;