let f be real-valued Function; :: thesis: ( f is bounded_above & f is bounded_below implies f is bounded )
assume f is bounded_above ; :: thesis: ( not f is bounded_below or f is bounded )
then consider r1 being real number such that
A5: for y being set st y in dom f holds
f . y < r1 by Def1;
assume f is bounded_below ; :: thesis: f is bounded
then consider r2 being real number such that
A6: for y being set st y in dom f holds
r2 < f . y by Def2;
take g = ((abs r1) + (abs r2)) + 1; :: according to SEQ_2:def 5 :: thesis: for y being set st y in dom f holds
abs (f . y) < g
A7: 0 <= abs r1 by COMPLEX1:46;
let y be set ; :: thesis: ( y in dom f implies abs (f . y) < g )
assume A8: y in dom f ; :: thesis: abs (f . y) < g
r1 <= abs r1 by ABSVALUE:4;
then f . y < abs r1 by A5, A8, XXREAL_0:2;
then (f . y) + 0 < (abs r1) + (abs r2) by COMPLEX1:46, XREAL_1:8;
then A9: f . y < g by XREAL_1:8;
- (abs r2) <= r2 by ABSVALUE:4;
then - (abs r2) < f . y by A6, A8, XXREAL_0:2;
then (- (abs r1)) + (- (abs r2)) < 0 + (f . y) by A7, XREAL_1:8;
then A10: ((- (abs r1)) - (abs r2)) + (- 1) < (f . y) + 0 by XREAL_1:8;
((- (abs r1)) - (abs r2)) - 1 = - g ;
hence abs (f . y) < g by A9, A10, Th9; :: thesis: verum