let Y be set ; :: thesis: for r being Real

for f being real-valued Function st f | Y is bounded holds

(r (#) f) | Y is bounded

let r be Real; :: thesis: for f being real-valued Function st f | Y is bounded holds

(r (#) f) | Y is bounded

let f be real-valued Function; :: thesis: ( f | Y is bounded implies (r (#) f) | Y is bounded )

assume A1: f | Y is bounded ; :: thesis: (r (#) f) | Y is bounded

for f being real-valued Function st f | Y is bounded holds

(r (#) f) | Y is bounded

let r be Real; :: thesis: for f being real-valued Function st f | Y is bounded holds

(r (#) f) | Y is bounded

let f be real-valued Function; :: thesis: ( f | Y is bounded implies (r (#) f) | Y is bounded )

assume A1: f | Y is bounded ; :: thesis: (r (#) f) | Y is bounded

per cases
( 0 <= r or r <= 0 )
;

end;

suppose A2:
0 <= r
; :: thesis: (r (#) f) | Y is bounded

hence
(r (#) f) | Y is bounded_above
by A1, Th78; :: according to SEQ_2:def 8 :: thesis: (r (#) f) | Y is bounded_below

thus (r (#) f) | Y is bounded_below by A1, A2, Th79; :: thesis: verum

end;thus (r (#) f) | Y is bounded_below by A1, A2, Th79; :: thesis: verum

suppose A3:
r <= 0
; :: thesis: (r (#) f) | Y is bounded

hence
(r (#) f) | Y is bounded_above
by A1, Th79; :: according to SEQ_2:def 8 :: thesis: (r (#) f) | Y is bounded_below

thus (r (#) f) | Y is bounded_below by A1, A3, Th78; :: thesis: verum

end;thus (r (#) f) | Y is bounded_below by A1, A3, Th78; :: thesis: verum