let f be PartFunc of REAL,REAL; :: thesis: ( f is convergent_in+infty & lim_in+infty f = 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 and
A2: lim_in+infty f = 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
g1 in dom f by A1;

now :: thesis: ex g2 being Real st
( r1 < g2 & g2 in dom (f ^) )

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

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

consider g2 being Real such that
A6: r < g2 and
A7: g2 in dom f by A1;
take g2 = g2; :: thesis: ( r1 < g2 & g2 in dom (f ^) )
g1 < g2 by A5, A6, XXREAL_0:2;
hence r1 < g2 by A4, XXREAL_0:2; :: thesis: g2 in dom (f ^)
g2 in { r2 where r2 is Real : r < r2 } by A6;
then g2 in right_open_halfline r by XXREAL_1:230;
then g2 in (dom f) /\ (right_open_halfline r) by A7, XBOOLE_0:def 4;
then 0 <> f . g2 by A3;
then not f . g2 in {0} by TARSKI:def 1;
then not g2 in f " {0} by FUNCT_1:def 7;
then g2 in (dom f) \ (f " {0}) by A7, XBOOLE_0:def 5;
hence g2 in dom (f ^) by RFUNCT_1:def 2; :: thesis: verum

end;

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

consider g2 being Real such that
A9: g1 < g2 and
A10: g2 in dom f by A1;
take g2 = g2; :: thesis: ( r1 < g2 & g2 in dom (f ^) )
thus r1 < g2 by A4, A9, XXREAL_0:2; :: thesis: g2 in dom (f ^)
r < g2 by A8, A9, XXREAL_0:2;
then g2 in { r2 where r2 is Real : r < r2 } ;
then g2 in right_open_halfline r by XXREAL_1:230;
then g2 in (dom f) /\ (right_open_halfline r) by A10, XBOOLE_0:def 4;
then 0 <> f . g2 by A3;
then not f . g2 in {0} by TARSKI:def 1;
then not g2 in f " {0} by FUNCT_1:def 7;
then g2 in (dom f) \ (f " {0}) by A10, XBOOLE_0:def 5;
hence g2 in dom (f ^) by RFUNCT_1:def 2; :: thesis: verum

end;

end;

end;

hence ex g1 being Real st
( r1 < g1 & g1 in dom (f ^) ) ; :: 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
A11: s is divergent_to+infty and
A12: rng s c= dom (f ^) ; :: thesis: (f ^) /* s is divergent_to+infty
consider k being Nat such that
A13: for n being Nat st k <= n holds
r < s . n by A11;
A14: rng (s ^\ k) c= rng s by VALUED_0:21;
dom (f ^) = (dom f) \ (f " {0}) by RFUNCT_1:def 2;
then A15: dom (f ^) c= dom f by XBOOLE_1:36;
then A16: rng s c= dom f by A12;
then A17: rng (s ^\ k) c= dom f by A14;

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

let n be Nat; :: thesis: 0 < (f /* (s ^\ k)) . n
A18: n in NAT by ORDINAL1:def 12;
r < s . (n + k) by A13, 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 A17, XBOOLE_0:def 4;
then 0 < f . ((s ^\ k) . n) by A3;
hence 0 < (f /* (s ^\ k)) . n by A16, A14, FUNCT_2:108, XBOOLE_1:1, A18; :: thesis: verum

end;

then A19: for n being Nat st 0 <= n holds
0 < (f /* (s ^\ k)) . n ;
s ^\ k is divergent_to+infty by A11, Th26;
then ( f /* (s ^\ k) is convergent & lim (f /* (s ^\ k)) = 0 ) by A1, A2, A17, Def12;
then A20: (f /* (s ^\ k)) " is divergent_to+infty by A19, Th35;
(f /* (s ^\ k)) " = ((f /* s) ^\ k) " by A12, A15, VALUED_0:27, XBOOLE_1:1
.= ((f /* s) ") ^\ k by SEQM_3:18
.= ((f ^) /* s) ^\ k by A12, RFUNCT_2:12 ;
hence (f ^) /* s is divergent_to+infty by A20, Th7; :: thesis: verum