let x0 be Real; :: thesis:
let f be PartFunc of REAL,REAL; :: thesis:
assume that
A1: f is_convergent_in x0 and
A2: lim (f,x0) = 0 and
A3: for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f & f . g1 <> 0 & f . g2 <> 0 ) ; :: thesis:
given r being Real such that A4: 0 < r and
A5: for g being Real st g in (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) holds
f . g <= 0 ; :: thesis:
thus for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (f ^) & g2 < r2 & x0 < g2 & g2 in dom (f ^) ) :: according to LIMFUNC3:def 3 :: thesis:

let r1, r2 be Real; :: thesis:
assume that
A6: r1 < x0 and
A7: x0 < r2 ; :: thesis:
consider g1, g2 being Real such that
A8: r1 < g1 and
A9: g1 < x0 and
A10: g1 in dom f and
A11: g2 < r2 and
A12: x0 < g2 and
A13: g2 in dom f and
A14: f . g1 <> 0 and
A15: f . g2 <> 0 by A3, A6, A7;
not f . g2 in {0} by A15, TARSKI:def 1;
then not g2 in f " {0} by FUNCT_1:def 7;
then A16: g2 in (dom f) \ (f " {0}) by A13, XBOOLE_0:def 5;
take g1 ; :: thesis:
take g2 ; :: thesis:
not f . g1 in {0} by A14, TARSKI:def 1;
then not g1 in f " {0} by FUNCT_1:def 7;
then g1 in (dom f) \ (f " {0}) by A10, XBOOLE_0:def 5;
hence ( r1 < g1 & g1 < x0 & g1 in dom (f ^) & g2 < r2 & x0 < g2 & g2 in dom (f ^) ) by A8, A9, A11, A12, A16, RFUNCT_1:def 2; :: thesis:

end;

let s be Real_Sequence; :: thesis:
assume that
A17: s is convergent and
A18: lim s = x0 and
A19: rng s c= (dom (f ^)) \ {x0} ; :: thesis:
consider k being Element of NAT such that
A20: for n being Element of NAT st k <= n holds
( x0 - r < s . n & s . n < x0 + r ) by A4, A17, A18, Th7;
A21: rng s c= dom (f ^) by A19, XBOOLE_1:1;
A22: dom (f ^) = (dom f) \ (f " {0}) by RFUNCT_1:def 2;
then A23: (f /* (s ^\ k)) " = ((f /* s) ^\ k) " by A21, VALUED_0:27, XBOOLE_1:1
.= ((f /* s) ") ^\ k by SEQM_3:18
.= ((f ^) /* s) ^\ k by A19, RFUNCT_2:12, XBOOLE_1:1 ;
A24: rng (s ^\ k) c= rng s by VALUED_0:21;
A25: rng s c= dom f by A21, A22, XBOOLE_1:1;
then A26: rng (s ^\ k) c= dom f by A24;
A27: rng (s ^\ k) c= (dom (f ^)) \ {x0} by A19, A24;
A28: rng (s ^\ k) c= (dom f) \ {x0}

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A29: x in rng (s ^\ k) ; :: thesis:
then not x in {x0} by A27, XBOOLE_0:def 5;
hence x in (dom f) \ {x0} by A26, A29, XBOOLE_0:def 5; :: thesis:

end;

A30: lim (s ^\ k) = x0 by A17, A18, SEQ_4:20;
then A31: lim (f /* (s ^\ k)) = 0 by A1, A2, A17, A28, Def4;
A32: f /* (s ^\ k) is non-zero by A21, A24, RFUNCT_2:11, XBOOLE_1:1;

A33: now :: thesis:

let n be Element of NAT ; :: thesis:
A34: k <= n + k by NAT_1:12;
then s . (n + k) < x0 + r by A20;
then A35: (s ^\ k) . n < x0 + r by NAT_1:def 3;
x0 - r < s . (n + k) by A20, A34;
then x0 - r < (s ^\ k) . n by NAT_1:def 3;
then (s ^\ k) . n in { g1 where g1 is Real : ( x0 - r < g1 & g1 < x0 + r ) } by A35;
then A36: (s ^\ k) . n in ].(x0 - r),(x0 + r).[ by RCOMP_1:def 2;
A37: (s ^\ k) . n in rng (s ^\ k) by VALUED_0:28;
then not (s ^\ k) . n in {x0} by A27, XBOOLE_0:def 5;
then (s ^\ k) . n in ].(x0 - r),(x0 + r).[ \ {x0} by A36, XBOOLE_0:def 5;
then (s ^\ k) . n in ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ by A4, Th4;
then (s ^\ k) . n in (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) by A26, A37, XBOOLE_0:def 4;
then A38: f . ((s ^\ k) . n) <= 0 by A5;
(f /* (s ^\ k)) . n <> 0 by A32, SEQ_1:5;
hence (f /* (s ^\ k)) . n < 0 by A25, A24, A38, FUNCT_2:108, XBOOLE_1:1; :: thesis:

end;

A39: for n being Nat st 0 <= n holds
(f /* (s ^\ k)) . n < 0

let n be Nat; :: thesis:
n in NAT by ORDINAL1:def 12;
hence ( 0 <= n implies (f /* (s ^\ k)) . n < 0 ) by A33; :: thesis:

end;

f /* (s ^\ k) is convergent by A1, A17, A30, A28;
then (f /* (s ^\ k)) " is divergent_to-infty by A31, A39, LIMFUNC1:36;
hence (f ^) /* s is divergent_to-infty by A23, LIMFUNC1:7; :: thesis: