let x0 be Real; :: thesis: for f being PartFunc of REAL,REAL st ex r being Real st
( f | ].x0,(x0 + r).[ is non-increasing & not f | ].x0,(x0 + r).[ is bounded_above ) & ( 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
( f | ].x0,(x0 + r).[ is non-increasing & not f | ].x0,(x0 + r).[ is bounded_above ) & ( 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: f | ].x0,(x0 + r).[ is non-increasing and
A2: not f | ].x0,(x0 + r).[ is bounded_above ; :: 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 5 :: 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 that
A3: seq is convergent and
A4: lim seq = x0 and
A5: rng seq c= (dom f) /\ (right_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) /\ (right_open_halfline x0) c= dom f by XBOOLE_1:17;
consider g1 being object such that
A7: g1 in ].x0,(x0 + r).[ /\ (dom f) and
A8: t < f . g1 by A2, RFUNCT_1:70;
reconsider g1 = g1 as Real by A7;
g1 in ].x0,(x0 + r).[ by A7, XBOOLE_0:def 4;
then g1 in { r1 where r1 is Real : ( x0 < r1 & r1 < x0 + r ) } by RCOMP_1:def 2;
then A9: ex r1 being Real st
( r1 = g1 & x0 < r1 & r1 < x0 + r ) ;
then consider n being Nat such that
A10: for k being Nat st n <= k holds
seq . k < g1 by A3, A4, Th2;
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 )
seq . k in rng seq by VALUED_0:28;
then A11: seq . k in (dom f) /\ (right_open_halfline x0) by A5;
(dom f) /\ (right_open_halfline x0) c= right_open_halfline x0 by XBOOLE_1:17;
then seq . k in right_open_halfline x0 by A11;
then seq . k in { r2 where r2 is Real : x0 < r2 } by XXREAL_1:230;
then A12: ex r2 being Real st
( r2 = seq . k & x0 < r2 ) ;
A13: k in NAT by ORDINAL1:def 12;
assume n <= k ; :: thesis: t < (f /* seq) . k
then A14: seq . k < g1 by A10;
then seq . k < x0 + r by A9, XXREAL_0:2;
then seq . k in { g2 where g2 is Real : ( x0 < g2 & g2 < x0 + r ) } by A12;
then seq . k in ].x0,(x0 + r).[ by RCOMP_1:def 2;
then seq . k in ].x0,(x0 + r).[ /\ (dom f) by A11, A6, XBOOLE_0:def 4;
then f . g1 <= f . (seq . k) by A1, A7, A14, RFUNCT_2:23;
then t < f . (seq . k) by A8, XXREAL_0:2;
hence t < (f /* seq) . k by A5, A6, FUNCT_2:108, XBOOLE_1:1, A13; :: thesis: verum
end;
hence f /* seq is divergent_to+infty ; :: thesis: verum