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 ;
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 ;
then A6: (f . c) + 0 <= |.r1.| + |.r2.| by ;
A7: 0 <= |.r1.| by COMPLEX1:46;
- |.r2.| <= r2 by ABSVALUE:4;
then - |.r2.| <= f . c by ;
then A8: (- |.r1.|) + (- |.r2.|) <= 0 + (f . c) by ;
(- |.r1.|) + (- |.r2.|) = - g ;
hence |.(f . c).| <= g by ; :: 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:
proof
take r + 1 ; :: according to SEQ_2:def 1 :: thesis: for b1 being object holds
( not b1 in dom f or not r + 1 <= f . b1 )

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 ;
f . c <= |.(f . c).| by ABSVALUE:4;
hence not r + 1 <= f . c by ; :: thesis: verum
end;
take - (r + 1) ; :: according to SEQ_2:def 2 :: thesis: for b1 being object holds
( not b1 in dom f or not f . b1 <= - (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 ;
then A11: - (r + 1) < - |.(f . c).| by XREAL_1:24;
- |.(f . c).| <= f . c by ABSVALUE:4;
hence not f . c <= - (r + 1) by ; :: thesis: verum