let x0 be Real; :: thesis: for f being PartFunc of REAL ,REAL st ex r being Real st
( 0 < r & f | ].(x0 - r),x0.[ is non-decreasing & not f | ].(x0 - r),x0.[ is bounded_above ) & ( for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom f ) ) holds
f is_left_divergent_to+infty_in x0
let f be PartFunc of REAL ,REAL ; :: thesis: ( ex r being Real st
( 0 < r & f | ].(x0 - r),x0.[ is non-decreasing & not f | ].(x0 - r),x0.[ is bounded_above ) & ( for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom f ) ) implies f is_left_divergent_to+infty_in x0 )
given r being Real such that A1: ( 0 < r & f | ].(x0 - r),x0.[ is non-decreasing & not f | ].(x0 - r),x0.[ is bounded_above ) ; :: thesis: ( ex r being Real st
( r < x0 & ( for g being Real holds
( not r < g or not g < x0 or not g in dom f ) ) ) or f is_left_divergent_to+infty_in x0 )
assume for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom f ) ; :: thesis: f is_left_divergent_to+infty_in x0
hence for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom f ) ; :: according to LIMFUNC2:def 2 :: thesis: for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (left_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) /\ (left_open_halfline x0) implies f /* seq is divergent_to+infty )
assume A2: ( seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (left_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
t < (f /* seq) . k
consider g1 being set such that
A3: ( g1 in ].(x0 - r),x0.[ /\ (dom f) & t < f . g1 ) by A1, RFUNCT_1:87;
reconsider g1 = g1 as Real by A3;
g1 in ].(x0 - r),x0.[ by A3, XBOOLE_0:def 4;
then g1 in { r1 where r1 is Real : ( x0 - r < r1 & r1 < x0 ) } by RCOMP_1:def 2;
then A4: ex r1 being Real st
( r1 = g1 & x0 - r < r1 & r1 < x0 ) ;
then consider n being Element of NAT such that
A5: for k being Element of NAT st n <= k holds
g1 < seq . k by A2, Th1;
take n = n; :: thesis: for k being Element of NAT st n <= k holds
t < (f /* seq) . k
let k be Element of NAT ; :: thesis: ( n <= k implies t < (f /* seq) . k )
seq . k in rng seq by VALUED_0:28;
then A6: seq . k in (dom f) /\ (left_open_halfline x0) by A2;
assume n <= k ; :: thesis: t < (f /* seq) . k
then A7: g1 < seq . k by A5;
then A8: x0 - r < seq . k by A4, XXREAL_0:2;
A9: ( (dom f) /\ (left_open_halfline x0) c= dom f & (dom f) /\ (left_open_halfline x0) c= left_open_halfline x0 ) by XBOOLE_1:17;
then ( seq . k in dom f & seq . k in left_open_halfline x0 ) by A6;
then seq . k in { r2 where r2 is Real : r2 < x0 } by XXREAL_1:229;
then ex r2 being Real st
( r2 = seq . k & r2 < x0 ) ;
then seq . k in { g2 where g2 is Real : ( x0 - r < g2 & g2 < x0 ) } by A8;
then seq . k in ].(x0 - r),x0.[ by RCOMP_1:def 2;
then seq . k in ].(x0 - r),x0.[ /\ (dom f) by A6, A9, XBOOLE_0:def 4;
then f . g1 <= f . (seq . k) by A1, A3, A7, RFUNCT_2:45;
then t < f . (seq . k) by A3, XXREAL_0:2;
hence t < (f /* seq) . k by A2, A9, FUNCT_2:185, XBOOLE_1:1; :: thesis: verum

end;

hence f /* seq is divergent_to+infty by LIMFUNC1:def 4; :: thesis: verum