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 such that
A5: for y being object st y in dom f holds
f . y < r1 ;
assume f is bounded_below ; :: thesis: f is bounded
then consider r2 being Real such that
A6: for y being object st y in dom f holds
r2 < f . y ;
take g = (|.r1.| + |.r2.|) + 1; :: according to COMSEQ_2:def 3 :: thesis: for b₁ being set holds
( not R15(b₁, dom f) or not g <= |.(f . b₁).| )
A7: 0 <= |.r1.| by COMPLEX1:46;
let y be set ; :: thesis: ( not R15(y, dom f) or not g <= |.(f . y).| )
assume A8: y in dom f ; :: thesis: not g <= |.(f . y).|
r1 <= |.r1.| by ABSVALUE:4;
then f . y < |.r1.| by A5, A8, XXREAL_0:2;
then (f . y) + 0 < |.r1.| + |.r2.| by COMPLEX1:46, XREAL_1:8;
then A9: f . y < g by XREAL_1:8;
- |.r2.| <= r2 by ABSVALUE:4;
then - |.r2.| < f . y by A6, A8, XXREAL_0:2;
then (- |.r1.|) + (- |.r2.|) < 0 + (f . y) by A7, XREAL_1:8;
then A10: ((- |.r1.|) - |.r2.|) + (- 1) < (f . y) + 0 by XREAL_1:8;
((- |.r1.|) - |.r2.|) - 1 = - g ;
hence |.(f . y).| < g by A9, A10, Th1; :: thesis: verum