let r be real number ; :: 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 Element of NAT ; :: according to SEQM_3:def 12 :: thesis: (r (#) seq) . n > (r (#) seq) . (n + 1)
seq . (n + 1) < seq . n by A1, Lm7;
then r * (seq . (n + 1)) < r * (seq . n) by A2, XREAL_1:70;
then (r (#) seq) . (n + 1) < r * (seq . n) by SEQ_1:13;
hence (r (#) seq) . n > (r (#) seq) . (n + 1) by SEQ_1:13; :: thesis: verum

end;

assume that
A3: seq is decreasing and
A4: r < 0 ; :: thesis: r (#) seq is increasing
let n be Element of NAT ; :: according to SEQM_3:def 11 :: thesis: (r (#) seq) . n < (r (#) seq) . (n + 1)
seq . (n + 1) < seq . n by A3, Lm7;
then r * (seq . n) < r * (seq . (n + 1)) by A4, XREAL_1:71;
then (r (#) seq) . n < r * (seq . (n + 1)) by SEQ_1:13;
hence (r (#) seq) . n < (r (#) seq) . (n + 1) by SEQ_1:13; :: thesis: verum