let r be real number ; :: 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

let n be Element of NAT ; :: thesis: (r (#) seq) . n < 1
(r (#) seq) . n = 0 * (seq . n) by A1, SEQ_1:13;
hence (r (#) seq) . n < 1 ; :: thesis: verum

end;

hence r (#) seq is bounded_above by SEQ_2:def 3; :: 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 Element of NAT holds not (r (#) seq) . b₁ <= p
let n be Element of NAT ; :: thesis: not (r (#) seq) . n <= p
( - 1 < 0 & r * (seq . n) = 0 ) by A1;
hence p < (r (#) seq) . n by SEQ_1:13; :: thesis: verum

end;

assume that
A2: seq is bounded_above and
A3: r < 0 ; :: thesis: r (#) seq is bounded_below
consider r1 being real number such that
A4: for n being Element of NAT holds seq . n < r1 by A2, SEQ_2:def 3;
take p = r * (abs r1); :: according to SEQ_2:def 4 :: thesis: for b₁ being Element of NAT holds not (r (#) seq) . b₁ <= p
let n be Element of NAT ; :: thesis: not (r (#) seq) . n <= p
r1 <= abs r1 by ABSVALUE:11;
then seq . n < abs r1 by A4, XXREAL_0:2;
then r * (abs r1) < r * (seq . n) by A3, XREAL_1:71;
hence p < (r (#) seq) . n by SEQ_1:13; :: thesis: verum