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
A2: 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
A3: 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
A4: 0 <= abs r1 by COMPLEX1:132;
let y be set ; :: thesis: ( y in dom f implies abs (f . y) < g )
assume Z: y in dom f ; :: thesis: abs (f . y) < g
r1 <= abs r1 by ABSVALUE:11;
then f . y < abs r1 by A2, XXREAL_0:2, Z;
then (f . y) + 0 < (abs r1) + (abs r2) by COMPLEX1:132, XREAL_1:10;
then A5: f . y < g by XREAL_1:10;
A6: - (abs r2) <= r2 by ABSVALUE:11;
A7: - (abs r1) <= - 0 by A4;
- (abs r2) < f . y by A3, A6, XXREAL_0:2, Z;
then (- (abs r1)) + (- (abs r2)) < 0 + (f . y) by A7, XREAL_1:10;
then A8: ((- (abs r1)) - (abs r2)) + (- 1) < (f . y) + 0 by XREAL_1:10;
((- (abs r1)) - (abs r2)) - 1 = - g ;
hence abs (f . y) < g by A5, A8, Th9; :: thesis: verum