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

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 A3: ( seq is divergent_to-infty & 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
A4: ( g1 in (left_open_halfline r1) /\ (dom f) & r < f . g1 ) by A1, RFUNCT_1:87;
reconsider g1 = g1 as Real by A4;
consider n being Element of NAT such that
A5: for m being Element of NAT st n <= m holds
seq . m < (- (abs r1)) - (abs g1) by A3, Def5;
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 )
A6: seq . m in rng seq by VALUED_0:28;
assume n <= m ; :: thesis: r < (f /* seq) . m
then A7: seq . m < (- (abs r1)) - (abs g1) by A5;
A8: - (abs r1) <= r1 by ABSVALUE:11;
0 <= abs g1 by COMPLEX1:132;
then (- (abs r1)) - (abs g1) <= r1 - 0 by A8, XREAL_1:15;
then seq . m < r1 by A7, XXREAL_0:2;
then seq . m in { g2 where g2 is Real : g2 < r1 } ;
then seq . m in left_open_halfline r1 by XXREAL_1:229;
then A9: seq . m in (left_open_halfline r1) /\ (dom f) by A3, A6, XBOOLE_0:def 4;
A10: - (abs g1) <= g1 by ABSVALUE:11;
0 <= abs r1 by COMPLEX1:132;
then (- (abs g1)) - (abs r1) <= g1 - 0 by A10, XREAL_1:15;
then seq . m < g1 by A7, XXREAL_0:2;
then f . g1 <= f . (seq . m) by A1, A4, A9, RFUNCT_2:46;
then r < f . (seq . m) by A4, XXREAL_0:2;
hence r < (f /* seq) . m by A3, FUNCT_2:185; :: thesis: verum

end;

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

end;

hence f is divergent_in-infty_to+infty by A2, Def10; :: thesis: verum