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

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