let Y be set ; :: thesis: for f being real-valued Function holds
( f | Y is bounded iff ex r being real number st
for c being set st c in Y /\ (dom f) holds
abs (f . c) <= r )
let f be real-valued Function; :: thesis: ( f | Y is bounded iff ex r being real number st
for c being set st c in Y /\ (dom f) holds
abs (f . c) <= r )
thus ( f | Y is bounded implies ex r being real number st
for c being set st c in Y /\ (dom f) holds
abs (f . c) <= r ) :: thesis: ( ex r being real number st
for c being set st c in Y /\ (dom f) holds
abs (f . c) <= r implies f | Y is bounded )

proof

assume A1: f | Y is bounded ; :: thesis: ex r being real number st
for c being set st c in Y /\ (dom f) holds
abs (f . c) <= r
then consider r1 being real number such that
A2: for c being set st c in Y /\ (dom f) holds
f . c <= r1 by Def9;
consider r2 being real number such that
A3: for c being set st c in Y /\ (dom f) holds
r2 <= f . c by A1, Def10;
take g = (abs r1) + (abs r2); :: thesis: for c being set st c in Y /\ (dom f) holds
abs (f . c) <= g
let c be set ; :: thesis: ( c in Y /\ (dom f) implies abs (f . c) <= g )
assume A4: c in Y /\ (dom f) ; :: thesis: abs (f . c) <= g
A5: 0 <= abs r1 by COMPLEX1:132;
A6: 0 <= abs r2 by COMPLEX1:132;
A7: r1 <= abs r1 by ABSVALUE:11;
f . c <= r1 by A2, A4;
then f . c <= abs r1 by A7, XXREAL_0:2;
then A8: (f . c) + 0 <= (abs r1) + (abs r2) by A6, XREAL_1:9;
A9: - (abs r2) <= r2 by ABSVALUE:11;
r2 <= f . c by A3, A4;
then - (abs r2) <= f . c by A9, XXREAL_0:2;
then A11: (- (abs r1)) + (- (abs r2)) <= 0 + (f . c) by A5, XREAL_1:9;
(- (abs r1)) + (- (abs r2)) = - g ;
hence abs (f . c) <= g by A8, A11, ABSVALUE:12; :: thesis: verum

end;

given r being real number such that A12: for c being set st c in Y /\ (dom f) holds
abs (f . c) <= r ; :: thesis: f | Y is bounded

now

let c be set ; :: thesis: ( c in Y /\ (dom f) implies f . c <= r )
assume c in Y /\ (dom f) ; :: thesis: f . c <= r
then A13: abs (f . c) <= r by A12;
f . c <= abs (f . c) by ABSVALUE:11;
hence f . c <= r by A13, XXREAL_0:2; :: thesis: verum

end;

then A14: f | Y is bounded_above by Def9;

now

let c be set ; :: thesis: ( c in Y /\ (dom f) implies - r <= f . c )
assume c in Y /\ (dom f) ; :: thesis: - r <= f . c
then abs (f . c) <= r by A12;
then A15: - r <= - (abs (f . c)) by XREAL_1:26;
- (abs (f . c)) <= f . c by ABSVALUE:11;
hence - r <= f . c by A15, XXREAL_0:2; :: thesis: verum

end;

then f | Y is bounded_below by Def10;
hence f | Y is bounded by A14; :: thesis: verum