for Y being set
for r being Real
for f being real-valued Function holds
( ( f | Y is bounded_above & 0 <= r implies (r (#) f) | Y is bounded_above ) & ( f | Y is bounded_above & r <= 0 implies (r (#) f) | Y is bounded_below ) )