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

proof

let r1 be object ; :: thesis: ( r1 in dom (f | (left_open_halfline r)) implies (- 1) + g < (f | (left_open_halfline r)) . r1 )
assume A3: r1 in dom (f | (left_open_halfline r)) ; :: thesis: (- 1) + g < (f | (left_open_halfline r)) . r1
then reconsider r1 = r1 as Real ;
r1 in (dom f) /\ (left_open_halfline r) by A3, RELAT_1:61;
then A4: ( r1 in dom f & r1 in left_open_halfline r ) by XBOOLE_0:def 4;
then |.((f . r1) - g).| < 1 by A2, XXREAL_1:233;
then A5: - 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 A2, A4, XXREAL_1:233; :: thesis: verum

end;

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

end;

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

proof

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

end;

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