let Y be set ; :: thesis:
let f be real-valued Function; :: thesis:
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:

assume A1: f | Y is bounded ; :: thesis:
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:
A4: r1 <= |.r1.| by ABSVALUE:4;
let c be object ; :: thesis:
assume A5: c in Y /\ (dom f) ; :: thesis:
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:

end;

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

let c be object ; :: thesis:
assume c in Y /\ (dom f) ; :: thesis:
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:

end;

then A13: f | Y is bounded_below by Th71;

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

end;

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