let R be FinSequence of REAL ; :: thesis: ( ( len R = 0 or len R = 1 ) implies R is non-increasing )
assume A1: ( len R = 0 or len R = 1 ) ; :: thesis: R is non-increasing

now

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

case len R = 0 ; :: thesis: R is non-increasing

then R = <*> REAL ;
then for n being Element of NAT st n in dom R & n + 1 in dom R holds
R . n >= R . (n + 1) ;
hence R is non-increasing by Def4; :: thesis: verum

end;

case len R = 1 ; :: thesis: R is non-increasing

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

now

let n be Element of NAT ; :: thesis: ( n in dom R & n + 1 in dom R implies R . n >= R . (n + 1) )
assume ( n in dom R & n + 1 in dom R ) ; :: thesis: R . n >= R . (n + 1)
then ( n = 1 & n + 1 = 1 ) by A2, TARSKI:def 1;
hence R . n >= R . (n + 1) ; :: thesis: verum

end;

hence R is non-increasing by Def4; :: thesis: verum

end;

end;

end;

hence R is non-increasing ; :: thesis: verum