let f be PartFunc of REAL,REAL; :: thesis: ( f is divergent_in+infty_to+infty implies ex r being Real st f | (right_open_halfline r) is bounded_below )
assume f is divergent_in+infty_to+infty ; :: thesis: ex r being Real st f | (right_open_halfline r) is bounded_below
then consider r being Real such that
A1: for r1 being Real st r < r1 & r1 in dom f holds
1 < f . r1 by LIMFUNC1:46;
for r1 being object st r1 in dom (f | (right_open_halfline r)) holds
1 < (f | (right_open_halfline r)) . r1
proof
let r1 be object ; :: thesis: ( r1 in dom (f | (right_open_halfline r)) implies 1 < (f | (right_open_halfline r)) . r1 )
assume A2: r1 in dom (f | (right_open_halfline r)) ; :: thesis: 1 < (f | (right_open_halfline r)) . r1
then reconsider r1 = r1 as Real ;
r1 in (dom f) /\ (right_open_halfline r) by A2, RELAT_1:61;
then A3: ( r1 in dom f & r1 in right_open_halfline r ) by XBOOLE_0:def 4;
then r < r1 by XXREAL_1:4;
then 1 < f . r1 by A1, A3;
hence 1 < (f | (right_open_halfline r)) . r1 by A3, 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: verum