let Y be set ; :: thesis: for f being real-valued Function st f | Y is bounded holds
( (abs f) | Y is bounded & (- f) | Y is bounded )
let f be real-valued Function; :: thesis: ( f | Y is bounded implies ( (abs f) | Y is bounded & (- f) | Y is bounded ) )
assume A1: f | Y is bounded ; :: thesis: ( (abs f) | Y is bounded & (- f) | Y is bounded )
(abs f) | Y = abs (f | Y) by Th46;
hence (abs f) | Y is bounded by A1; :: thesis: (- f) | Y is bounded
thus (- f) | Y is bounded by A1, Th80; :: thesis: verum