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

( (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