let r be Real; :: thesis: for seq being Real_Sequence holds
( ( seq is bounded_above & 0 < r implies r (#) seq is bounded_above ) & ( 0 = r implies r (#) seq is bounded ) & ( seq is bounded_above & r < 0 implies r (#) seq is bounded_below ) )
let seq be Real_Sequence; :: thesis: ( ( seq is bounded_above & 0 < r implies r (#) seq is bounded_above ) & ( 0 = r implies r (#) seq is bounded ) & ( seq is bounded_above & r < 0 implies r (#) seq is bounded_below ) )
thus ( seq is bounded_above & 0 < r implies r (#) seq is bounded_above ) ; :: thesis: ( ( 0 = r implies r (#) seq is bounded ) & ( seq is bounded_above & r < 0 implies r (#) seq is bounded_below ) )
thus ( 0 = r implies r (#) seq is bounded ) :: thesis: ( seq is bounded_above & r < 0 implies r (#) seq is bounded_below )

proof

assume A1: 0 = r ; :: thesis: r (#) seq is bounded

now :: thesis: for n being Nat holds (r (#) seq) . n < 1

let n be Nat; :: thesis: (r (#) seq) . n < 1
(r (#) seq) . n = 0 * (seq . n) by A1, SEQ_1:9;
hence (r (#) seq) . n < 1 ; :: thesis: verum

end;

hence r (#) seq is bounded_above ; :: according to SEQ_2:def 8 :: thesis: r (#) seq is bounded_below
take p = - 1; :: according to SEQ_2:def 4 :: thesis: for b₁ being set holds not (r (#) seq) . b₁ <= p
let n be Nat; :: thesis: not (r (#) seq) . n <= p
( - 1 < 0 & r * (seq . n) = 0 ) by A1;
hence p < (r (#) seq) . n by SEQ_1:9; :: thesis: verum

end;

assume that
A2: seq is bounded_above and
A3: r < 0 ; :: thesis: r (#) seq is bounded_below
consider r1 being Real such that
A4: for n being Nat holds seq . n < r1 by A2;
take p = r * |.r1.|; :: according to SEQ_2:def 4 :: thesis: for b₁ being set holds not (r (#) seq) . b₁ <= p
let n be Nat; :: thesis: not (r (#) seq) . n <= p
r1 <= |.r1.| by ABSVALUE:4;
then seq . n < |.r1.| by A4, XXREAL_0:2;
then r * |.r1.| < r * (seq . n) by A3, XREAL_1:69;
hence p < (r (#) seq) . n by SEQ_1:9; :: thesis: verum