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 Th87;
consider r2 being real number such that
A3: for c being set st c in Y /\ (dom f) holds
r2 <= f . c by A1, Th88;
take g = (abs r1) + (abs r2); :: thesis: for c being set st c in Y /\ (dom f) holds
abs (f . c) <= g
A4: r1 <= abs r1 by ABSVALUE:4;
let c be set ; :: thesis: ( c in Y /\ (dom f) implies abs (f . c) <= g )
assume A5: c in Y /\ (dom f) ; :: thesis: abs (f . c) <= g
f . c <= r1 by A2, A5;
then A6: f . c <= abs r1 by A4, XXREAL_0:2;
A7: - (abs r2) <= r2 by ABSVALUE:4;
r2 <= f . c by A3, A5;
then A8: - (abs r2) <= f . c by A7, XXREAL_0:2;
0 <= abs r1 by COMPLEX1:46;
then A9: (- (abs r1)) + (- (abs r2)) <= 0 + (f . c) by A8, XREAL_1:7;
0 <= abs r2 by COMPLEX1:46;
then A10: (f . c) + 0 <= (abs r1) + (abs r2) by A6, XREAL_1:7;
(- (abs r1)) + (- (abs r2)) = - g ;
hence abs (f . c) <= g by A10, A9, ABSVALUE:5; :: thesis: verum

end;

given r being real number such that A11: 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 - r <= f . c )
assume c in Y /\ (dom f) ; :: thesis: - r <= f . c
then abs (f . c) <= r by A11;
then A12: - r <= - (abs (f . c)) by XREAL_1:24;
- (abs (f . c)) <= f . c by ABSVALUE:4;
hence - r <= f . c by A12, XXREAL_0:2; :: thesis: verum

end;

then A13: f | Y is bounded_below by Th88;

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 A14: abs (f . c) <= r by A11;
f . c <= abs (f . c) by ABSVALUE:4;
hence f . c <= r by A14, XXREAL_0:2; :: thesis: verum

end;

then f | Y is bounded_above by Th87;
hence f | Y is bounded by A13; :: thesis: verum