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
per cases ( 0 <= r or r <= 0 ) ;
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;
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;
end;