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

proof

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

end;

given r being real number such that A9: for c being set st c in dom f holds
abs (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 set holds
( not b₁ in proj1 f or not r + 1 <= K250(f,b₁) )
let c be set ; :: thesis: ( not c in proj1 f or not r + 1 <= K250(f,c) )
assume c in dom f ; :: thesis: not r + 1 <= K250(f,c)
then A10: abs (f . c) < r + 1 by A9, XREAL_1:39;
f . c <= abs (f . c) by ABSVALUE:4;
hence not r + 1 <= K250(f,c) by A10, XXREAL_0:2; :: thesis: verum

end;

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