let x0 be Real; :: thesis: for f being PartFunc of REAL ,REAL st f is_left_convergent_in x0 & lim_left f,x0 = 0 & ex r being Real st
( 0 < r & ( for g being Real st g in (dom f) /\ ].(x0 - r),x0.[ holds
0 < f . g ) ) holds
f ^ is_left_divergent_to+infty_in x0
let f be PartFunc of REAL ,REAL ; :: thesis: ( f is_left_convergent_in x0 & lim_left f,x0 = 0 & ex r being Real st
( 0 < r & ( for g being Real st g in (dom f) /\ ].(x0 - r),x0.[ holds
0 < f . g ) ) implies f ^ is_left_divergent_to+infty_in x0 )
assume that
A1: f is_left_convergent_in x0 and
A2: lim_left f,x0 = 0 ; :: thesis: ( for r being Real holds
( not 0 < r or ex g being Real st
( g in (dom f) /\ ].(x0 - r),x0.[ & not 0 < f . g ) ) or f ^ is_left_divergent_to+infty_in x0 )
given r being Real such that A3: 0 < r and
A4: for g being Real st g in (dom f) /\ ].(x0 - r),x0.[ holds
0 < f . g ; :: thesis: f ^ is_left_divergent_to+infty_in x0
thus for r1 being Real st r1 < x0 holds
ex g1 being Real st
( r1 < g1 & g1 < x0 & g1 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

proof

let r1 be Real; :: thesis: ( r1 < x0 implies ex g1 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (f ^ ) ) )
assume r1 < x0 ; :: thesis: ex g1 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (f ^ ) )
then consider g1 being Real such that
A5: r1 < g1 and
A6: g1 < x0 and
g1 in dom f by A1, Def1;

now

per cases ( g1 <= x0 - r or x0 - r <= g1 ) ;

suppose A7: g1 <= x0 - r ; :: thesis: ex g2 being Real st
( r1 < g2 & g2 < x0 & g2 in dom (f ^ ) )

x0 - r < x0 by A3, Lm1;
then consider g2 being Real such that
A8: x0 - r < g2 and
A9: g2 < x0 and
A10: g2 in dom f by A1, Def1;
take g2 = g2; :: thesis: ( r1 < g2 & g2 < x0 & g2 in dom (f ^ ) )
g1 < g2 by A7, A8, XXREAL_0:2;
hence ( r1 < g2 & g2 < x0 ) by A5, A9, XXREAL_0:2; :: thesis: g2 in dom (f ^ )
g2 in { r2 where r2 is Real : ( x0 - r < r2 & r2 < x0 ) } by A8, A9;
then g2 in ].(x0 - r),x0.[ by RCOMP_1:def 2;
then g2 in (dom f) /\ ].(x0 - r),x0.[ by A10, XBOOLE_0:def 4;
then 0 <> f . g2 by A4;
then not f . g2 in {0 } by TARSKI:def 1;
then not g2 in f " {0 } by FUNCT_1:def 13;
then g2 in (dom f) \ (f " {0 }) by A10, XBOOLE_0:def 5;
hence g2 in dom (f ^ ) by RFUNCT_1:def 8; :: thesis: verum

end;

suppose A11: x0 - r <= g1 ; :: thesis: ex g2 being Real st
( r1 < g2 & g2 < x0 & g2 in dom (f ^ ) )

consider g2 being Real such that
A12: g1 < g2 and
A13: g2 < x0 and
A14: g2 in dom f by A1, A6, Def1;
take g2 = g2; :: thesis: ( r1 < g2 & g2 < x0 & g2 in dom (f ^ ) )
thus ( r1 < g2 & g2 < x0 ) by A5, A12, A13, XXREAL_0:2; :: thesis: g2 in dom (f ^ )
x0 - r < g2 by A11, A12, XXREAL_0:2;
then g2 in { r2 where r2 is Real : ( x0 - r < r2 & r2 < x0 ) } by A13;
then g2 in ].(x0 - r),x0.[ by RCOMP_1:def 2;
then g2 in (dom f) /\ ].(x0 - r),x0.[ by A14, XBOOLE_0:def 4;
then 0 <> f . g2 by A4;
then not f . g2 in {0 } by TARSKI:def 1;
then not g2 in f " {0 } by FUNCT_1:def 13;
then g2 in (dom f) \ (f " {0 }) by A14, XBOOLE_0:def 5;
hence g2 in dom (f ^ ) by RFUNCT_1:def 8; :: thesis: verum

end;

end;

end;

hence ex g1 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (f ^ ) ) ; :: thesis: verum

end;

let s be Real_Sequence; :: thesis: ( s is convergent & lim s = x0 & rng s c= (dom (f ^ )) /\ (left_open_halfline x0) implies (f ^ ) /* s is divergent_to+infty )
assume that
A15: s is convergent and
A16: lim s = x0 and
A17: rng s c= (dom (f ^ )) /\ (left_open_halfline x0) ; :: thesis: (f ^ ) /* s is divergent_to+infty
x0 - r < x0 by A3, Lm1;
then consider k being Element of NAT such that
A18: for n being Element of NAT st k <= n holds
x0 - r < s . n by A15, A16, Th1;
A19: lim (s ^\ k) = x0 by A15, A16, SEQ_4:33;
dom (f ^ ) = (dom f) \ (f " {0 }) by RFUNCT_1:def 8;
then A20: dom (f ^ ) c= dom f by XBOOLE_1:36;
A21: rng (s ^\ k) c= rng s by VALUED_0:21;
(dom (f ^ )) /\ (left_open_halfline x0) c= left_open_halfline x0 by XBOOLE_1:17;
then rng s c= left_open_halfline x0 by A17, XBOOLE_1:1;
then A22: rng (s ^\ k) c= left_open_halfline x0 by A21, XBOOLE_1:1;
A23: (dom (f ^ )) /\ (left_open_halfline x0) c= dom (f ^ ) by XBOOLE_1:17;
then A24: rng s c= dom (f ^ ) by A17, XBOOLE_1:1;
then A25: rng s c= dom f by A20, XBOOLE_1:1;
then A26: rng (s ^\ k) c= dom f by A21, XBOOLE_1:1;
then A27: rng (s ^\ k) c= (dom f) /\ (left_open_halfline x0) by A22, XBOOLE_1:19;
then A28: lim (f /* (s ^\ k)) = 0 by A1, A2, A15, A19, Def7;

now

let n be Element of NAT ; :: thesis: 0 < (f /* (s ^\ k)) . n
x0 - r < s . (n + k) by A18, NAT_1:12;
then A29: x0 - r < (s ^\ k) . n by NAT_1:def 3;
A30: (s ^\ k) . n in rng (s ^\ k) by VALUED_0:28;
then (s ^\ k) . n in left_open_halfline x0 by A22;
then (s ^\ k) . n in { g1 where g1 is Real : g1 < x0 } by XXREAL_1:229;
then ex g1 being Real st
( g1 = (s ^\ k) . n & g1 < x0 ) ;
then (s ^\ k) . n in { g2 where g2 is Real : ( x0 - r < g2 & g2 < x0 ) } by A29;
then (s ^\ k) . n in ].(x0 - r),x0.[ by RCOMP_1:def 2;
then (s ^\ k) . n in (dom f) /\ ].(x0 - r),x0.[ by A26, A30, XBOOLE_0:def 4;
then 0 < f . ((s ^\ k) . n) by A4;
hence 0 < (f /* (s ^\ k)) . n by A25, A21, FUNCT_2:185, XBOOLE_1:1; :: thesis: verum

end;

then A31: for n being Element of NAT st 0 <= n holds
0 < (f /* (s ^\ k)) . n ;
f /* (s ^\ k) is convergent by A1, A2, A15, A19, A27, Def7;
then A32: (f /* (s ^\ k)) " is divergent_to+infty by A28, A31, LIMFUNC1:62;
(f /* (s ^\ k)) " = ((f /* s) ^\ k) " by A24, A20, VALUED_0:27, XBOOLE_1:1
.= ((f /* s) " ) ^\ k by SEQM_3:41
.= ((f ^ ) /* s) ^\ k by A17, A23, RFUNCT_2:27, XBOOLE_1:1 ;
hence (f ^ ) /* s is divergent_to+infty by A32, LIMFUNC1:34; :: thesis: verum