let f be PartFunc of REAL,REAL; :: thesis: ( ex r being Real st
( f | (right_open_halfline r) is non-decreasing & not f | (right_open_halfline r) is bounded_above ) & ( for r being Real ex g being Real st
( r < g & g in dom f ) ) implies f is divergent_in+infty_to+infty )
given r1 being Real such that A1: f | (right_open_halfline r1) is non-decreasing and
A2: not f | (right_open_halfline r1) is bounded_above ; :: thesis: ( ex r being Real st
for g being Real holds
( not r < g or not g in dom f ) or f is divergent_in+infty_to+infty )

A3: now

let seq be Real_Sequence; :: thesis: ( seq is divergent_to+infty & rng seq c= dom f implies f /* seq is divergent_to+infty )
assume that
A4: seq is divergent_to+infty and
A5: rng seq c= dom f ; :: thesis: f /* seq is divergent_to+infty

now

let r be Real; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
r < (f /* seq) . m
consider g1 being set such that
A6: g1 in (right_open_halfline r1) /\ (dom f) and
A7: r < f . g1 by A2, RFUNCT_1:70;
reconsider g1 = g1 as Real by A6;
consider n being Element of NAT such that
A8: for m being Element of NAT st n <= m holds
(abs g1) + (abs r1) < seq . m by A4, Def4;
take n = n; :: thesis: for m being Element of NAT st n <= m holds
r < (f /* seq) . m
let m be Element of NAT ; :: thesis: ( n <= m implies r < (f /* seq) . m )
assume n <= m ; :: thesis: r < (f /* seq) . m
then A9: (abs g1) + (abs r1) < seq . m by A8;
( r1 <= abs r1 & 0 <= abs g1 ) by ABSVALUE:4, COMPLEX1:46;
then 0 + r1 <= (abs g1) + (abs r1) by XREAL_1:7;
then r1 < seq . m by A9, XXREAL_0:2;
then seq . m in { g2 where g2 is Real : r1 < g2 } ;
then ( seq . m in rng seq & seq . m in right_open_halfline r1 ) by VALUED_0:28, XXREAL_1:230;
then A10: seq . m in (right_open_halfline r1) /\ (dom f) by A5, XBOOLE_0:def 4;
( g1 <= abs g1 & 0 <= abs r1 ) by ABSVALUE:4, COMPLEX1:46;
then g1 + 0 <= (abs g1) + (abs r1) by XREAL_1:7;
then g1 < seq . m by A9, XXREAL_0:2;
then f . g1 <= f . (seq . m) by A1, A6, A10, RFUNCT_2:22;
then r < f . (seq . m) by A7, XXREAL_0:2;
hence r < (f /* seq) . m by A5, FUNCT_2:108; :: thesis: verum

end;

hence f /* seq is divergent_to+infty by Def4; :: thesis: verum

end;

assume for r being Real ex g being Real st
( r < g & g in dom f ) ; :: thesis: f is divergent_in+infty_to+infty
hence f is divergent_in+infty_to+infty by A3, Def7; :: thesis: verum