let f be PartFunc of REAL,REAL; ( f is convergent_in-infty & lim_in-infty f = 0 & ex r being Real st
for g being Real st g in (dom f) /\ (left_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
; ( for r being Real ex g being Real st
( g in (dom f) /\ (left_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) /\ (left_open_halfline r) holds
0 < f . g
; f ^ is divergent_in-infty_to+infty
thus
for r1 being Real ex g1 being Real st
( g1 < r1 & g1 in dom (f ^) )
LIMFUNC1:def 10 for seq being Real_Sequence st seq is divergent_to-infty & rng seq c= dom (f ^) holds
(f ^) /* seq is divergent_to+infty
let s be Real_Sequence; ( 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 ^)
; (f ^) /* s is divergent_to+infty
consider k being Nat such that
A13:
for n being Nat st k <= n holds
s . n < r
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;
then A19:
for n being Nat st 0 <= n holds
0 < (f /* (s ^\ k)) . n
;
s ^\ k is divergent_to-infty
by A11, Th27;
then
( f /* (s ^\ k) is convergent & lim (f /* (s ^\ k)) = 0 )
by A1, A2, A17, Def13;
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; verum