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

proof

assume that
A1: seq is decreasing and
A2: 0 < r ; :: thesis: r (#) seq is decreasing
let n be Nat; :: according to SEQM_3:def 7 :: 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:68;
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 decreasing and
A4: r < 0 ; :: thesis: r (#) seq is increasing
let n be Nat; :: according to SEQM_3:def 6 :: 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:69;
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