theorem Th79: :: RFUNCT_1:79

for Y being set
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 ) )