let f be PartFunc of REAL ,REAL ; :: thesis: ( f is convergent_in+infty & lim_in+infty f = 0 & ( for r being Real ex g being Real st
( r < g & g in dom f & f . g <> 0 ) ) & ex r being Real st
for g being Real st g in (dom f) /\ (right_open_halfline r) holds
0 <= f . g implies f ^ is divergent_in+infty_to+infty )
assume that
A1: ( f is convergent_in+infty & lim_in+infty f = 0 ) and
A2: for r being Real ex g being Real st
( r < g & g in dom f & f . g <> 0 ) ; :: thesis: ( for r being Real ex g being Real st
( g in (dom f) /\ (right_open_halfline r) & not 0 <= f . g ) or f ^ is divergent_in+infty_to+infty )
given r being Real such that A3: for g being Real st g in (dom f) /\ (right_open_halfline r) holds
0 <= f . g ; :: thesis: f ^ is divergent_in+infty_to+infty
thus for r1 being Real ex g1 being Real st
( r1 < g1 & g1 in dom (f ^ ) ) :: according to LIMFUNC1:def 7 :: thesis: for seq being Real_Sequence st seq is divergent_to+infty & rng seq c= dom (f ^ ) holds
(f ^ ) /* seq is divergent_to+infty

proof

let r1 be Real; :: thesis: ex g1 being Real st
( r1 < g1 & g1 in dom (f ^ ) )
consider g1 being Real such that
A4: r1 < g1 and
A5: g1 in dom f and
A6: f . g1 <> 0 by A2;
take g1 ; :: thesis: ( r1 < g1 & g1 in dom (f ^ ) )
thus r1 < g1 by A4; :: thesis: g1 in dom (f ^ )
not f . g1 in {0 } by A6, TARSKI:def 1;
then not g1 in f " {0 } by FUNCT_1:def 13;
then g1 in (dom f) \ (f " {0 }) by A5, XBOOLE_0:def 5;
hence g1 in dom (f ^ ) by RFUNCT_1:def 8; :: thesis: verum

end;

let s be Real_Sequence; :: thesis: ( s is divergent_to+infty & rng s c= dom (f ^ ) implies (f ^ ) /* s is divergent_to+infty )
assume that
A7: s is divergent_to+infty and
A8: rng s c= dom (f ^ ) ; :: thesis: (f ^ ) /* s is divergent_to+infty
consider k being Element of NAT such that
A9: for n being Element of NAT st k <= n holds
r < s . n by A7, Def4;
A10: rng (s ^\ k) c= rng s by VALUED_0:21;
dom (f ^ ) = (dom f) \ (f " {0 }) by RFUNCT_1:def 8;
then A11: dom (f ^ ) c= dom f by XBOOLE_1:36;
then A12: rng s c= dom f by A8, XBOOLE_1:1;
then A13: rng (s ^\ k) c= dom f by A10, XBOOLE_1:1;
A14: f /* (s ^\ k) is non-zero by A8, A10, RFUNCT_2:26, XBOOLE_1:1;

now

let n be Element of NAT ; :: thesis: 0 < (f /* (s ^\ k)) . n
r < s . (n + k) by A9, NAT_1:12;
then r < (s ^\ k) . n by NAT_1:def 3;
then (s ^\ k) . n in { g2 where g2 is Real : r < g2 } ;
then ( (s ^\ k) . n in rng (s ^\ k) & (s ^\ k) . n in right_open_halfline r ) by VALUED_0:28, XXREAL_1:230;
then (s ^\ k) . n in (dom f) /\ (right_open_halfline r) by A13, XBOOLE_0:def 4;
then A15: 0 <= f . ((s ^\ k) . n) by A3;
(f /* (s ^\ k)) . n <> 0 by A14, SEQ_1:7;
hence 0 < (f /* (s ^\ k)) . n by A12, A10, A15, FUNCT_2:185, XBOOLE_1:1; :: thesis: verum

end;

then A16: for n being Element of NAT st 0 <= n holds
0 < (f /* (s ^\ k)) . n ;
s ^\ k is divergent_to+infty by A7, Th53;
then ( f /* (s ^\ k) is convergent & lim (f /* (s ^\ k)) = 0 ) by A1, A13, Def12;
then A17: (f /* (s ^\ k)) " is divergent_to+infty by A16, Th62;
(f /* (s ^\ k)) " = ((f /* s) ^\ k) " by A8, A11, VALUED_0:27, XBOOLE_1:1
.= ((f /* s) " ) ^\ k by SEQM_3:41
.= ((f ^ ) /* s) ^\ k by A8, RFUNCT_2:27 ;
hence (f ^ ) /* s is divergent_to+infty by A17, Th34; :: thesis: verum