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 ;
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 ;
A7: - |.r2.| <= r2 by ABSVALUE:4;
r2 <= f . c by A3, A5;
then A8: - |.r2.| <= f . c by ;
0 <= |.r1.| by COMPLEX1:46;
then A9: (- |.r1.|) + (- |.r2.|) <= 0 + (f . c) by ;
0 <= |.r2.| by COMPLEX1:46;
then A10: (f . c) + 0 <= |.r1.| + |.r2.| by ;
(- |.r1.|) + (- |.r2.|) = - g ;
hence |.(f . c).| <= g by ; :: 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 ; :: 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 ; :: thesis: verum
end;
then f | Y is bounded_above by Th70;
hence f | Y is bounded by A13; :: thesis: verum