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

assume A1: ( len R = 0 or len R = 1 ) ; :: thesis: R is non-increasing

now :: thesis: ( ( len R = 0 & R is non-increasing ) or ( len R = 1 & R is non-increasing ) )end;

hence
R is non-increasing
; :: thesis: verumper cases
( len R = 0 or len R = 1 )
by A1;

end;

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

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-increasing ; :: thesis: verum

end;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-increasing ; :: thesis: verum

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

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

end;now :: thesis: for n being Nat st n in dom R & n + 1 in dom R holds

R . n >= R . (n + 1)

hence
R is non-increasing
; :: thesis: verumR . 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;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