let x0 be Real; :: thesis: for f being PartFunc of REAL ,REAL st ex r being Real st
( 0 < r & f | ].x0,(x0 + r).[ is non-decreasing & not f | ].x0,(x0 + r).[ is bounded_below ) & ( for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom f ) ) holds
f is_right_divergent_to-infty_in x0
let f be PartFunc of REAL ,REAL ; :: thesis: ( ex r being Real st
( 0 < r & f | ].x0,(x0 + r).[ is non-decreasing & not f | ].x0,(x0 + r).[ is bounded_below ) & ( for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom f ) ) implies f is_right_divergent_to-infty_in x0 )
given r being Real such that A1: ( 0 < r & f | ].x0,(x0 + r).[ is non-decreasing & not f | ].x0,(x0 + r).[ is bounded_below ) ; :: thesis: ( ex r being Real st
( x0 < r & ( for g being Real holds
( not g < r or not x0 < g or not g in dom f ) ) ) or f is_right_divergent_to-infty_in x0 )
assume for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom f ) ; :: thesis: f is_right_divergent_to-infty_in x0
hence for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom f ) ; :: according to LIMFUNC2:def 6 :: thesis: for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (right_open_halfline x0) holds
f /* seq is divergent_to-infty
let seq be Real_Sequence; :: thesis: ( seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (right_open_halfline x0) implies f /* seq is divergent_to-infty )
assume A2: ( seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (right_open_halfline x0) ) ; :: thesis: f /* seq is divergent_to-infty

now

let t be Real; :: thesis: ex n being Element of NAT st
for k being Element of NAT st n <= k holds
(f /* seq) . k < t
consider g1 being set such that
A3: ( g1 in ].x0,(x0 + r).[ /\ (dom f) & f . g1 < t ) by A1, RFUNCT_1:88;
reconsider g1 = g1 as Real by A3;
g1 in ].x0,(x0 + r).[ by A3, XBOOLE_0:def 4;
then g1 in { r1 where r1 is Real : ( x0 < r1 & r1 < x0 + r ) } by RCOMP_1:def 2;
then A4: ex r1 being Real st
( r1 = g1 & x0 < r1 & r1 < x0 + r ) ;
then consider n being Element of NAT such that
A5: for k being Element of NAT st n <= k holds
seq . k < g1 by A2, Th2;
take n = n; :: thesis: for k being Element of NAT st n <= k holds
(f /* seq) . k < t
let k be Element of NAT ; :: thesis: ( n <= k implies (f /* seq) . k < t )
seq . k in rng seq by VALUED_0:28;
then A6: seq . k in (dom f) /\ (right_open_halfline x0) by A2;
assume n <= k ; :: thesis: (f /* seq) . k < t
then A7: seq . k < g1 by A5;
then A8: seq . k < x0 + r by A4, XXREAL_0:2;
A9: ( (dom f) /\ (right_open_halfline x0) c= dom f & (dom f) /\ (right_open_halfline x0) c= right_open_halfline x0 ) by XBOOLE_1:17;
then ( seq . k in dom f & seq . k in right_open_halfline x0 ) by A6;
then seq . k in { r2 where r2 is Real : x0 < r2 } by XXREAL_1:230;
then ex r2 being Real st
( r2 = seq . k & x0 < r2 ) ;
then seq . k in { g2 where g2 is Real : ( x0 < g2 & g2 < x0 + r ) } by A8;
then seq . k in ].x0,(x0 + r).[ by RCOMP_1:def 2;
then seq . k in ].x0,(x0 + r).[ /\ (dom f) by A6, A9, XBOOLE_0:def 4;
then f . (seq . k) <= f . g1 by A1, A3, A7, RFUNCT_2:45;
then f . (seq . k) < t by A3, XXREAL_0:2;
hence (f /* seq) . k < t by A2, A9, FUNCT_2:185, XBOOLE_1:1; :: thesis: verum

end;

hence f /* seq is divergent_to-infty by LIMFUNC1:def 5; :: thesis: verum