let x0 be Real; :: thesis: for f being PartFunc of REAL,REAL st f is_left_convergent_in x0 & lim_left (f,x0) = 0 & ( for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom f & f . g <> 0 ) ) & ex r being Real st
( 0 < r & ( for g being Real st g in (dom f) /\ ].(x0 - r),x0.[ holds
f . g <= 0 ) ) 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 & ( for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom f & f . g <> 0 ) ) & ex r being Real st
( 0 < r & ( for g being Real st g in (dom f) /\ ].(x0 - r),x0.[ holds
f . g <= 0 ) ) 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 and
A3: for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom f & f . g <> 0 ) ; :: thesis: ( for r being Real holds
( not 0 < r or ex g being Real st
( g in (dom f) /\ ].(x0 - r),x0.[ & not f . g <= 0 ) ) or f ^ is_left_divergent_to-infty_in x0 )
given r being Real such that A4: 0 < r and
A5: for g being Real st g in (dom f) /\ ].(x0 - r),x0.[ holds
f . g <= 0 ; :: 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 3 :: 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
A6: r1 < g1 and
A7: g1 < x0 and
A8: g1 in dom f and
A9: f . g1 <> 0 by A3;
take g1 ; :: thesis: ( r1 < g1 & g1 < x0 & g1 in dom (f ^) )
thus ( r1 < g1 & g1 < x0 ) by A6, A7; :: thesis: g1 in dom (f ^)
not f . g1 in {0} by A9, TARSKI:def 1;
then not g1 in f " {0} by FUNCT_1:def 7;
then g1 in (dom f) \ (f " {0}) by A8, XBOOLE_0:def 5;
hence g1 in dom (f ^) by RFUNCT_1:def 2; :: 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
A10: s is convergent and
A11: lim s = x0 and
A12: rng s c= (dom (f ^)) /\ (left_open_halfline x0) ; :: thesis: (f ^) /* s is divergent_to-infty
x0 - r < x0 by A4, Lm1;
then consider k being Nat such that
A13: for n being Nat st k <= n holds
x0 - r < s . n by A10, A11, Th1;
A14: lim (s ^\ k) = x0 by A10, A11, SEQ_4:20;
A15: (dom (f ^)) /\ (left_open_halfline x0) c= dom (f ^) by XBOOLE_1:17;
then A16: rng s c= dom (f ^) by A12, XBOOLE_1:1;
A17: rng (s ^\ k) c= rng s by VALUED_0:21;
dom (f ^) = (dom f) \ (f " {0}) by RFUNCT_1:def 2;
then A18: dom (f ^) c= dom f by XBOOLE_1:36;
then A19: rng s c= dom f by A16, XBOOLE_1:1;
then A20: rng (s ^\ k) c= dom f by A17, XBOOLE_1:1;
(dom (f ^)) /\ (left_open_halfline x0) c= left_open_halfline x0 by XBOOLE_1:17;
then rng s c= left_open_halfline x0 by A12, XBOOLE_1:1;
then A21: rng (s ^\ k) c= left_open_halfline x0 by A17, XBOOLE_1:1;
then A22: rng (s ^\ k) c= (dom f) /\ (left_open_halfline x0) by A20, XBOOLE_1:19;
then A23: lim (f /* (s ^\ k)) = 0 by A1, A2, A10, A14, Def7;
A24: f /* (s ^\ k) is non-zero by A16, A17, RFUNCT_2:11, XBOOLE_1:1;

now :: thesis: for n being Nat holds (f /* (s ^\ k)) . n < 0

let n be Nat; :: thesis: (f /* (s ^\ k)) . n < 0
A25: n in NAT by ORDINAL1:def 12;
x0 - r < s . (n + k) by A13, NAT_1:12;
then A26: x0 - r < (s ^\ k) . n by NAT_1:def 3;
A27: (s ^\ k) . n in rng (s ^\ k) by VALUED_0:28;
then (s ^\ k) . n in left_open_halfline x0 by A21;
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 A26;
then (s ^\ k) . n in ].(x0 - r),x0.[ by RCOMP_1:def 2;
then (s ^\ k) . n in (dom f) /\ ].(x0 - r),x0.[ by A20, A27, XBOOLE_0:def 4;
then A28: f . ((s ^\ k) . n) <= 0 by A5;
(f /* (s ^\ k)) . n <> 0 by A24, SEQ_1:5;
hence (f /* (s ^\ k)) . n < 0 by A19, A17, A28, FUNCT_2:108, XBOOLE_1:1, A25; :: thesis: verum

end;

then A29: for n being Nat st 0 <= n holds
(f /* (s ^\ k)) . n < 0 ;
f /* (s ^\ k) is convergent by A1, A10, A14, A22;
then A30: (f /* (s ^\ k)) " is divergent_to-infty by A23, A29, LIMFUNC1:36;
(f /* (s ^\ k)) " = ((f /* s) ^\ k) " by A16, A18, VALUED_0:27, XBOOLE_1:1
.= ((f /* s) ") ^\ k by SEQM_3:18
.= ((f ^) /* s) ^\ k by A12, A15, RFUNCT_2:12, XBOOLE_1:1 ;
hence (f ^) /* s is divergent_to-infty by A30, LIMFUNC1:7; :: thesis: verum