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

proof

assume A1: f | Y is bounded ; :: thesis: ex r being Real st
for c being object st c in Y /\ (dom f) holds
|.(f . c).| <= r
then consider r1 being Real such that
A2: for c being object st c in Y /\ (dom f) holds
f . c <= r1 by Th70;
consider r2 being Real such that
A3: for c being object st c in Y /\ (dom f) holds
r2 <= f . c by A1, Th71;
take g = |.r1.| + |.r2.|; :: thesis: for c being object st c in Y /\ (dom f) holds
|.(f . c).| <= g
A4: r1 <= |.r1.| by ABSVALUE:4;
let c be object ; :: thesis: ( c in Y /\ (dom f) implies |.(f . c).| <= g )
assume A5: c in Y /\ (dom f) ; :: thesis: |.(f . c).| <= g
f . c <= r1 by A2, A5;
then A6: f . c <= |.r1.| by A4, XXREAL_0:2;
A7: - |.r2.| <= r2 by ABSVALUE:4;
r2 <= f . c by A3, A5;
then A8: - |.r2.| <= f . c by A7, XXREAL_0:2;
0 <= |.r1.| by COMPLEX1:46;
then A9: (- |.r1.|) + (- |.r2.|) <= 0 + (f . c) by A8, XREAL_1:7;
0 <= |.r2.| by COMPLEX1:46;
then A10: (f . c) + 0 <= |.r1.| + |.r2.| by A6, XREAL_1:7;
(- |.r1.|) + (- |.r2.|) = - g ;
hence |.(f . c).| <= g by A10, A9, ABSVALUE:5; :: thesis: verum

end;

given r being Real such that A11: for c being object st c in Y /\ (dom f) holds
|.(f . c).| <= r ; :: thesis: f | Y is bounded

now :: thesis: for c being object st c in Y /\ (dom f) holds
- r <= f . c

let c be object ; :: thesis: ( c in Y /\ (dom f) implies - r <= f . c )
assume c in Y /\ (dom f) ; :: thesis: - r <= f . c
then |.(f . c).| <= r by A11;
then A12: - r <= - |.(f . c).| by XREAL_1:24;
- |.(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 Th71;

now :: thesis: for c being object st c in Y /\ (dom f) holds
f . c <= r

let c be object ; :: thesis: ( c in Y /\ (dom f) implies f . c <= r )
assume c in Y /\ (dom f) ; :: thesis: f . c <= r
then A14: |.(f . c).| <= r by A11;
f . c <= |.(f . c).| by ABSVALUE:4;
hence f . c <= r by A14, XXREAL_0:2; :: thesis: verum

end;

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