let r be Real; :: thesis: for seq being Real_Sequence holds
( ( seq is non-increasing & 0 <= r implies r (#) seq is non-increasing ) & ( seq is non-increasing & r <= 0 implies r (#) seq is non-decreasing ) )
let seq be Real_Sequence; :: thesis: ( ( seq is non-increasing & 0 <= r implies r (#) seq is non-increasing ) & ( seq is non-increasing & r <= 0 implies r (#) seq is non-decreasing ) )
thus ( seq is non-increasing & 0 <= r implies r (#) seq is non-increasing ) :: thesis: ( seq is non-increasing & r <= 0 implies r (#) seq is non-decreasing )

proof

assume that
A1: seq is non-increasing and
A2: 0 <= r ; :: thesis: r (#) seq is non-increasing
let n be Nat; :: according to SEQM_3:def 9 :: thesis: (r (#) seq) . n >= (r (#) seq) . (n + 1)
seq . (n + 1) <= seq . n by A1;
then r * (seq . (n + 1)) <= r * (seq . n) by A2, XREAL_1:64;
then (r (#) seq) . (n + 1) <= r * (seq . n) by SEQ_1:9;
hence (r (#) seq) . n >= (r (#) seq) . (n + 1) by SEQ_1:9; :: thesis: verum

end;

assume that
A3: seq is non-increasing and
A4: r <= 0 ; :: thesis: r (#) seq is non-decreasing
let n be Nat; :: according to SEQM_3:def 8 :: thesis: (r (#) seq) . n <= (r (#) seq) . (n + 1)
seq . (n + 1) <= seq . n by A3;
then r * (seq . n) <= r * (seq . (n + 1)) by A4, XREAL_1:65;
then (r (#) seq) . n <= r * (seq . (n + 1)) by SEQ_1:9;
hence (r (#) seq) . n <= (r (#) seq) . (n + 1) by SEQ_1:9; :: thesis: verum