let x0 be Real; :: thesis: for f being PartFunc of REAL,REAL st ex r being Real st
( 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
( 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: f | ].(x0 - r),x0.[ is non-decreasing and
A2: 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 that
A3: seq is convergent and
A4: lim seq = x0 and
A5: rng seq c= (dom f) /\ (left_open_halfline x0) ; :: thesis: f /* seq is divergent_to+infty

now :: thesis: for t being Real ex n being Nat st
for k being Nat st n <= k holds
t < (f /* seq) . k

let t be Real; :: thesis: ex n being Nat st
for k being Nat st n <= k holds
t < (f /* seq) . k
A6: (dom f) /\ (left_open_halfline x0) c= dom f by XBOOLE_1:17;
consider g1 being object such that
A7: g1 in ].(x0 - r),x0.[ /\ (dom f) and
A8: t < f . g1 by A2, RFUNCT_1:70;
reconsider g1 = g1 as Real by A7;
g1 in ].(x0 - r),x0.[ by A7, XBOOLE_0:def 4;
then g1 in { r1 where r1 is Real : ( x0 - r < r1 & r1 < x0 ) } by RCOMP_1:def 2;
then A9: ex r1 being Real st
( r1 = g1 & x0 - r < r1 & r1 < x0 ) ;
then consider n being Nat such that
A10: for k being Nat st n <= k holds
g1 < seq . k by A3, A4, Th1;
take n = n; :: thesis: for k being Nat st n <= k holds
t < (f /* seq) . k
let k be Nat; :: thesis: ( n <= k implies t < (f /* seq) . k )
A11: k in NAT by ORDINAL1:def 12;
seq . k in rng seq by VALUED_0:28;
then A12: seq . k in (dom f) /\ (left_open_halfline x0) by A5;
(dom f) /\ (left_open_halfline x0) c= left_open_halfline x0 by XBOOLE_1:17;
then seq . k in left_open_halfline x0 by A12;
then seq . k in { r2 where r2 is Real : r2 < x0 } by XXREAL_1:229;
then A13: ex r2 being Real st
( r2 = seq . k & r2 < x0 ) ;
assume n <= k ; :: thesis: t < (f /* seq) . k
then A14: g1 < seq . k by A10;
then x0 - r < seq . k by A9, XXREAL_0:2;
then seq . k in { g2 where g2 is Real : ( x0 - r < g2 & g2 < x0 ) } by A13;
then seq . k in ].(x0 - r),x0.[ by RCOMP_1:def 2;
then seq . k in ].(x0 - r),x0.[ /\ (dom f) by A12, A6, XBOOLE_0:def 4;
then f . g1 <= f . (seq . k) by A1, A7, A14, RFUNCT_2:22;
then t < f . (seq . k) by A8, XXREAL_0:2;
hence t < (f /* seq) . k by A5, A6, FUNCT_2:108, XBOOLE_1:1, A11; :: thesis: verum

end;

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