let Y be set ; :: thesis: for r being Real
for f being real-valued Function holds
( ( f | Y is bounded_below & 0 <= r implies (r (#) f) | Y is bounded_below ) & ( f | Y is bounded_below & r <= 0 implies (r (#) f) | Y is bounded_above ) )
let r be Real; :: thesis: for f being real-valued Function holds
( ( f | Y is bounded_below & 0 <= r implies (r (#) f) | Y is bounded_below ) & ( f | Y is bounded_below & r <= 0 implies (r (#) f) | Y is bounded_above ) )
let f be real-valued Function; :: thesis: ( ( f | Y is bounded_below & 0 <= r implies (r (#) f) | Y is bounded_below ) & ( f | Y is bounded_below & r <= 0 implies (r (#) f) | Y is bounded_above ) )
(r (#) f) | Y = r (#) (f | Y) by Th49;
hence ( ( f | Y is bounded_below & 0 <= r implies (r (#) f) | Y is bounded_below ) & ( f | Y is bounded_below & r <= 0 implies (r (#) f) | Y is bounded_above ) ) ; :: thesis: verum