let f be real-valued Function; :: thesis: ( f is bounded implies ( f is bounded_above & f is bounded_below ) )
given r being real number such that A1: for y being set st y in dom f holds
abs (f . y) < r ; :: according to SEQ_2:def 5 :: 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 set st y in dom f holds
f . y < r
let y be set ; :: thesis: ( y in dom f implies f . y < r )
A2: f . y <= abs (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 - (abs r) ; :: according to SEQ_2:def 2 :: thesis: for y being set st y in dom f holds
- (abs r) < f . y
let y be set ; :: thesis: ( y in dom f implies - (abs r) < f . y )
A3: - (abs (f . y)) <= f . y by ABSVALUE:4;
r <= abs r by ABSVALUE:4;
then A4: - (abs r) <= - r by XREAL_1:24;
assume y in dom f ; :: thesis: - (abs r) < f . y
then abs (f . y) < r by A1;
then - r < - (abs (f . y)) by XREAL_1:24;
then - (abs r) < - (abs (f . y)) by A4, XXREAL_0:2;
hence - (abs r) < f . y by A3, XXREAL_0:2; :: thesis: verum