let f be PartFunc of REAL,REAL; :: thesis: ( f is convergent_in+infty implies ( ex r being Real st f | (right_open_halfline r) is bounded_below & ex r being Real st f | (right_open_halfline r) is bounded_above ) )
assume A1: f is convergent_in+infty ; :: thesis: ( ex r being Real st f | (right_open_halfline r) is bounded_below & ex r being Real st f | (right_open_halfline r) is bounded_above )
consider g being Real such that
A2: for g1 being Real st 0 < g1 holds
ex r being Real st
for r1 being Real st r < r1 & r1 in dom f holds
|.((f . r1) - g).| < g1 by A1, LIMFUNC1:44;
consider r being Real such that
A3: for r1 being Real st r < r1 & r1 in dom f holds
|.((f . r1) - g).| < 1 by A2;
for r1 being object st r1 in dom (f | (right_open_halfline r)) holds
(- 1) + g < (f | (right_open_halfline r)) . r1

proof

let r1 be object ; :: thesis: ( r1 in dom (f | (right_open_halfline r)) implies (- 1) + g < (f | (right_open_halfline r)) . r1 )
assume A4: r1 in dom (f | (right_open_halfline r)) ; :: thesis: (- 1) + g < (f | (right_open_halfline r)) . r1
then reconsider r1 = r1 as Real ;
r1 in (dom f) /\ (right_open_halfline r) by A4, RELAT_1:61;
then A5: ( r1 in dom f & r1 in right_open_halfline r ) by XBOOLE_0:def 4;
then |.((f . r1) - g).| < 1 by A3, XXREAL_1:235;
then A6: - 1 <= (f . r1) - g by ABSVALUE:5;

now :: thesis: not - 1 = (f . r1) - g

assume - 1 = (f . r1) - g ; :: thesis: contradiction
then |.((f . r1) - g).| = - (- 1) by ABSVALUE:def 1;
hence contradiction by A3, A5, XXREAL_1:235; :: thesis: verum

end;

then - 1 < (f . r1) - g by A6, XXREAL_0:1;
then (- 1) + g < f . r1 by XREAL_1:20;
hence (- 1) + g < (f | (right_open_halfline r)) . r1 by A5, FUNCT_1:49; :: thesis: verum

end;

then f | (right_open_halfline r) is bounded_below by SEQ_2:def 2;
hence ex r being Real st f | (right_open_halfline r) is bounded_below ; :: thesis: ex r being Real st f | (right_open_halfline r) is bounded_above
consider r being Real such that
A7: for r1 being Real st r < r1 & r1 in dom f holds
|.((f . r1) - g).| < 1 by A2;
for r1 being object st r1 in dom (f | (right_open_halfline r)) holds
(f | (right_open_halfline r)) . r1 < g + 1

proof

let r1 be object ; :: thesis: ( r1 in dom (f | (right_open_halfline r)) implies (f | (right_open_halfline r)) . r1 < g + 1 )
assume A8: r1 in dom (f | (right_open_halfline r)) ; :: thesis: (f | (right_open_halfline r)) . r1 < g + 1
then reconsider r1 = r1 as Real ;
r1 in (dom f) /\ (right_open_halfline r) by A8, RELAT_1:61;
then A9: ( r1 in dom f & r1 in right_open_halfline r ) by XBOOLE_0:def 4;
then |.((f . r1) - g).| < 1 by A7, XXREAL_1:235;
then (f . r1) - g < 1 by ABSVALUE:def 1;
then f . r1 < g + 1 by XREAL_1:19;
hence (f | (right_open_halfline r)) . r1 < g + 1 by A9, FUNCT_1:49; :: thesis: verum

end;

then f | (right_open_halfline r) is bounded_above by SEQ_2:def 1;
hence ex r being Real st f | (right_open_halfline r) is bounded_above ; :: thesis: verum