let f be PartFunc of REAL,REAL; ( f is convergent_in-infty & lim_in-infty f = 0 & ( for r being Real ex g being Real st
( g < r & g in dom f & f . g <> 0 ) ) & ex r being Real st
for g being Real st g in (dom f) /\ (left_open_halfline r) holds
f . g <= 0 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
( g < r & g in dom f & f . g <> 0 )
; ( for r being Real ex g being Real st
( g in (dom f) /\ (left_open_halfline r) & not f . g <= 0 ) 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
f . g <= 0
; 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 11 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
A7:
s is divergent_to-infty
and
A8:
rng s c= dom (f ^)
; (f ^) /* s is divergent_to-infty
consider k being Nat such that
A9:
for n being Nat st k <= n holds
s . n < r
by A7;
A10:
rng (s ^\ k) c= rng s
by VALUED_0:21;
dom (f ^) = (dom f) \ (f " {0})
by RFUNCT_1:def 2;
then A11:
dom (f ^) c= dom f
by XBOOLE_1:36;
then A12:
rng s c= dom f
by A8;
then A13:
rng (s ^\ k) c= dom f
by A10;
A14:
f /* (s ^\ k) is non-zero
by A8, A10, RFUNCT_2:11, XBOOLE_1:1;
then A17:
for n being Nat st 0 <= n holds
(f /* (s ^\ k)) . n < 0
;
s ^\ k is divergent_to-infty
by A7, Th27;
then
( f /* (s ^\ k) is convergent & lim (f /* (s ^\ k)) = 0 )
by A1, A13, Def13;
then A18:
(f /* (s ^\ k)) " is divergent_to-infty
by A17, Th36;
(f /* (s ^\ k)) " =
((f /* s) ^\ k) "
by A8, A11, VALUED_0:27, XBOOLE_1:1
.=
((f /* s) ") ^\ k
by SEQM_3:18
.=
((f ^) /* s) ^\ k
by A8, RFUNCT_2:12
;
hence
(f ^) /* s is divergent_to-infty
by A18, Th7; verum