let f be PartFunc of REAL,REAL; :: thesis: ( f is divergent_in-infty_to-infty implies ex r being Real st f | (left_open_halfline r) is bounded_above )
assume A1: f is divergent_in-infty_to-infty ; :: thesis: ex r being Real st f | (left_open_halfline r) is bounded_above
consider r being Real such that
A2: for r1 being Real st r1 < r & r1 in dom f holds
f . r1 < 1 by A1, LIMFUNC1:49;
for r1 being object st r1 in dom (f | (left_open_halfline r)) holds
(f | (left_open_halfline r)) . r1 < 1

proof

let r1 be object ; :: thesis: ( r1 in dom (f | (left_open_halfline r)) implies (f | (left_open_halfline r)) . r1 < 1 )
assume A3: r1 in dom (f | (left_open_halfline r)) ; :: thesis: (f | (left_open_halfline r)) . r1 < 1
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 r1 < r by XXREAL_1:4;
then f . r1 < 1 by A2, A4;
hence (f | (left_open_halfline r)) . r1 < 1 by A4, 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