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

proof

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

end;

given r being Real such that A9: for c being object st c in dom f holds
|.(f . c).| <= r ; :: thesis: f is bounded
thus f is bounded_above :: according to SEQ_2:def 8 :: thesis: f is bounded_below

proof

take r + 1 ; :: according to SEQ_2:def 1 :: thesis: for b₁ being object holds
( not b₁ in dom f or not r + 1 <= f . b₁ )
let c be object ; :: thesis: ( not c in dom f or not r + 1 <= f . c )
assume c in dom f ; :: thesis: not r + 1 <= f . c
then A10: |.(f . c).| < r + 1 by A9, XREAL_1:39;
f . c <= |.(f . c).| by ABSVALUE:4;
hence not r + 1 <= f . c by A10, XXREAL_0:2; :: thesis: verum

end;

take - (r + 1) ; :: according to SEQ_2:def 2 :: thesis: for b₁ being object holds
( not b₁ in dom f or not f . b₁ <= - (r + 1) )
let c be object ; :: thesis: ( not c in dom f or not f . c <= - (r + 1) )
assume c in dom f ; :: thesis: not f . c <= - (r + 1)
then |.(f . c).| < r + 1 by A9, XREAL_1:39;
then A11: - (r + 1) < - |.(f . c).| by XREAL_1:24;
- |.(f . c).| <= f . c by ABSVALUE:4;
hence not f . c <= - (r + 1) by A11, XXREAL_0:2; :: thesis: verum