let x0 be Real; :: thesis:
let f be PartFunc of REAL ,REAL ; :: thesis:
assume A1: ( f is_right_convergent_in x0 & lim_right f,x0 = 0 & ( for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom f & f . g <> 0 ) ) ) ; :: thesis:
given r being Real such that A2: ( 0 < r & ( for g being Real st g in (dom f) /\ ].x0,(x0 + r).[ holds
f . g <= 0 ) ) ; :: thesis:
thus for r1 being Real st x0 < r1 holds
ex g1 being Real st
( g1 < r1 & x0 < g1 & g1 in dom (f ^ ) ) :: according to LIMFUNC2:def 6 :: thesis:

proof

let r1 be Real; :: thesis:
assume x0 < r1 ; :: thesis:
then consider g1 being Real such that
A3: ( g1 < r1 & x0 < g1 & g1 in dom f & f . g1 <> 0 ) by A1;
take g1 ; :: thesis:
thus ( g1 < r1 & x0 < g1 ) by A3; :: thesis:
not f . g1 in {0 } by A3, TARSKI:def 1;
then not g1 in f " {0 } by FUNCT_1:def 13;
then g1 in (dom f) \ (f " {0 }) by A3, XBOOLE_0:def 5;
hence g1 in dom (f ^ ) by RFUNCT_1:def 8; :: thesis:

end;

let s be Real_Sequence; :: thesis:
assume A4: ( s is convergent & lim s = x0 & rng s c= (dom (f ^ )) /\ (right_open_halfline x0) ) ; :: thesis:
x0 < x0 + r by A2, Lm1;
then consider k being Element of NAT such that
A5: for n being Element of NAT st k <= n holds
s . n < x0 + r by A4, Th2;
A6: ( s ^\ k is convergent & lim (s ^\ k) = x0 ) by A4, SEQ_4:33;
A7: ( (dom (f ^ )) /\ (right_open_halfline x0) c= dom (f ^ ) & (dom (f ^ )) /\ (right_open_halfline x0) c= right_open_halfline x0 ) by XBOOLE_1:17;
then A8: ( rng s c= dom (f ^ ) & rng s c= right_open_halfline x0 ) by A4, XBOOLE_1:1;
dom (f ^ ) = (dom f) \ (f " {0 }) by RFUNCT_1:def 8;
then A9: dom (f ^ ) c= dom f by XBOOLE_1:36;
then A10: rng s c= dom f by A8, XBOOLE_1:1;
A11: rng (s ^\ k) c= rng s by VALUED_0:21;
then A12: ( rng (s ^\ k) c= (dom (f ^ )) /\ (right_open_halfline x0) & rng (s ^\ k) c= dom (f ^ ) & rng (s ^\ k) c= right_open_halfline x0 & rng (s ^\ k) c= dom f ) by A4, A8, A10, XBOOLE_1:1;
then rng (s ^\ k) c= (dom f) /\ (right_open_halfline x0) by XBOOLE_1:19;
then A13: ( f /* (s ^\ k) is convergent & lim (f /* (s ^\ k)) = 0 ) by A1, A6, Def8;
A14: f /* (s ^\ k) is non-zero by A8, A11, RFUNCT_2:26, XBOOLE_1:1;

A15: now

let n be Element of NAT ; :: thesis:
A16: (s ^\ k) . n in rng (s ^\ k) by VALUED_0:28;
then (s ^\ k) . n in right_open_halfline x0 by A12;
then (s ^\ k) . n in { g1 where g1 is Real : x0 < g1 } by XXREAL_1:230;
then A17: ex g1 being Real st
( g1 = (s ^\ k) . n & x0 < g1 ) ;
s . (n + k) < x0 + r by A5, NAT_1:12;
then (s ^\ k) . n < x0 + r by NAT_1:def 3;
then (s ^\ k) . n in { g2 where g2 is Real : ( x0 < g2 & g2 < x0 + r ) } by A17;
then (s ^\ k) . n in ].x0,(x0 + r).[ by RCOMP_1:def 2;
then (s ^\ k) . n in (dom f) /\ ].x0,(x0 + r).[ by A12, A16, XBOOLE_0:def 4;
then A18: f . ((s ^\ k) . n) <= 0 by A2;
(f /* (s ^\ k)) . n <> 0 by A14, SEQ_1:7;
hence (f /* (s ^\ k)) . n < 0 by A10, A11, A18, FUNCT_2:185, XBOOLE_1:1; :: thesis:

end;

then for n being Element of NAT holds 0 <> (f /* (s ^\ k)) . n ;
then A19: f /* (s ^\ k) is non-zero by SEQ_1:7;
for n being Element of NAT st 0 <= n holds
(f /* (s ^\ k)) . n < 0 by A15;
then A20: (f /* (s ^\ k)) " is divergent_to-infty by A13, A19, LIMFUNC1:63;
(f /* (s ^\ k)) " = ((f /* s) ^\ k) " by A8, A9, VALUED_0:27, XBOOLE_1:1
.= ((f /* s) " ) ^\ k by SEQM_3:41
.= ((f ^ ) /* s) ^\ k by A4, A7, RFUNCT_2:27, XBOOLE_1:1 ;
hence (f ^ ) /* s is divergent_to-infty by A20, LIMFUNC1:34; :: thesis: