let f be real-valued Function; :: thesis: ( f is bounded implies ( f is bounded_above & f is bounded_below ) )
given r being Real such that A1: for y being set st y in dom f holds
|.(f . y).| < r ; :: according to COMSEQ_2:def 3 :: thesis: ( f is bounded_above & f is bounded_below )
thus f is bounded_above :: thesis: f is bounded_below

proof

take r ; :: according to SEQ_2:def 1 :: thesis: for y being object st y in dom f holds
f . y < r
let y be object ; :: thesis: ( y in dom f implies f . y < r )
A2: f . y <= |.(f . y).| by ABSVALUE:4;
assume y in dom f ; :: thesis: f . y < r
hence f . y < r by A1, A2, XXREAL_0:2; :: thesis: verum

end;

take - |.r.| ; :: according to SEQ_2:def 2 :: thesis: for y being object st y in dom f holds
- |.r.| < f . y
let y be object ; :: thesis: ( y in dom f implies - |.r.| < f . y )
A3: - |.(f . y).| <= f . y by ABSVALUE:4;
r <= |.r.| by ABSVALUE:4;
then A4: - |.r.| <= - r by XREAL_1:24;
assume y in dom f ; :: thesis: - |.r.| < f . y
then |.(f . y).| < r by A1;
then - r < - |.(f . y).| by XREAL_1:24;
then - |.r.| < - |.(f . y).| by A4, XXREAL_0:2;
hence - |.r.| < f . y by A3, XXREAL_0:2; :: thesis: verum