let x0 be Real; for f being PartFunc of REAL,REAL st f is_right_convergent_in x0 & lim_right (f,x0) = 0 & ( for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom f & f . g <> 0 ) ) & ex r being Real st
( 0 < r & ( for g being Real st g in (dom f) /\ ].x0,(x0 + r).[ holds
f . g <= 0 ) ) holds
f ^ is_right_divergent_to-infty_in x0
let f be PartFunc of REAL,REAL; ( f is_right_convergent_in x0 & lim_right (f,x0) = 0 & ( for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom f & f . g <> 0 ) ) & ex r being Real st
( 0 < r & ( for g being Real st g in (dom f) /\ ].x0,(x0 + r).[ holds
f . g <= 0 ) ) implies f ^ is_right_divergent_to-infty_in x0 )
assume that
A1:
f is_right_convergent_in x0
and
A2:
lim_right (f,x0) = 0
and
A3:
for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom f & f . g <> 0 )
; ( for r being Real holds
( not 0 < r or ex g being Real st
( g in (dom f) /\ ].x0,(x0 + r).[ & not f . g <= 0 ) ) or f ^ is_right_divergent_to-infty_in x0 )
given r being Real such that A4:
0 < r
and
A5:
for g being Real st g in (dom f) /\ ].x0,(x0 + r).[ holds
f . g <= 0
; f ^ is_right_divergent_to-infty_in x0
thus
for r1 being Real st x0 < r1 holds
ex g1 being Real st
( g1 < r1 & x0 < g1 & g1 in dom (f ^) )
LIMFUNC2:def 6 for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom (f ^)) /\ (right_open_halfline x0) holds
(f ^) /* seq is divergent_to-infty
let s be Real_Sequence; ( s is convergent & lim s = x0 & rng s c= (dom (f ^)) /\ (right_open_halfline x0) implies (f ^) /* s is divergent_to-infty )
assume that
A10:
s is convergent
and
A11:
lim s = x0
and
A12:
rng s c= (dom (f ^)) /\ (right_open_halfline x0)
; (f ^) /* s is divergent_to-infty
x0 < x0 + r
by A4, Lm1;
then consider k being Nat such that
A13:
for n being Nat st k <= n holds
s . n < x0 + r
by A10, A11, Th2;
A14:
lim (s ^\ k) = x0
by A10, A11, SEQ_4:20;
A15:
(dom (f ^)) /\ (right_open_halfline x0) c= dom (f ^)
by XBOOLE_1:17;
then A16:
rng s c= dom (f ^)
by A12, XBOOLE_1:1;
A17:
rng (s ^\ k) c= rng s
by VALUED_0:21;
dom (f ^) = (dom f) \ (f " {0})
by RFUNCT_1:def 2;
then A18:
dom (f ^) c= dom f
by XBOOLE_1:36;
then A19:
rng s c= dom f
by A16, XBOOLE_1:1;
then A20:
rng (s ^\ k) c= dom f
by A17, XBOOLE_1:1;
(dom (f ^)) /\ (right_open_halfline x0) c= right_open_halfline x0
by XBOOLE_1:17;
then
rng s c= right_open_halfline x0
by A12, XBOOLE_1:1;
then A21:
rng (s ^\ k) c= right_open_halfline x0
by A17, XBOOLE_1:1;
then A22:
rng (s ^\ k) c= (dom f) /\ (right_open_halfline x0)
by A20, XBOOLE_1:19;
then A23:
lim (f /* (s ^\ k)) = 0
by A1, A2, A10, A14, Def8;
A24:
f /* (s ^\ k) is non-zero
by A16, A17, RFUNCT_2:11, XBOOLE_1:1;
now for n being Nat holds (f /* (s ^\ k)) . n < 0 let n be
Nat;
(f /* (s ^\ k)) . n < 0 A25:
n in NAT
by ORDINAL1:def 12;
s . (n + k) < x0 + r
by A13, NAT_1:12;
then A26:
(s ^\ k) . n < x0 + r
by NAT_1:def 3;
A27:
(s ^\ k) . n in rng (s ^\ k)
by VALUED_0:28;
then
(s ^\ k) . n in right_open_halfline x0
by A21;
then
(s ^\ k) . n in { g1 where g1 is Real : x0 < g1 }
by XXREAL_1:230;
then
ex
g1 being
Real st
(
g1 = (s ^\ k) . n &
x0 < g1 )
;
then
(s ^\ k) . n in { g2 where g2 is Real : ( x0 < g2 & g2 < x0 + r ) }
by A26;
then
(s ^\ k) . n in ].x0,(x0 + r).[
by RCOMP_1:def 2;
then
(s ^\ k) . n in (dom f) /\ ].x0,(x0 + r).[
by A20, A27, XBOOLE_0:def 4;
then A28:
f . ((s ^\ k) . n) <= 0
by A5;
(f /* (s ^\ k)) . n <> 0
by A24, SEQ_1:5;
hence
(f /* (s ^\ k)) . n < 0
by A19, A17, A28, FUNCT_2:108, XBOOLE_1:1, A25;
verum end;
then A29:
for n being Nat st 0 <= n holds
(f /* (s ^\ k)) . n < 0
;
f /* (s ^\ k) is convergent
by A1, A10, A14, A22;
then A30:
(f /* (s ^\ k)) " is divergent_to-infty
by A23, A29, LIMFUNC1:36;
(f /* (s ^\ k)) " =
((f /* s) ^\ k) "
by A16, A18, VALUED_0:27, XBOOLE_1:1
.=
((f /* s) ") ^\ k
by SEQM_3:18
.=
((f ^) /* s) ^\ k
by A12, A15, RFUNCT_2:12, XBOOLE_1:1
;
hence
(f ^) /* s is divergent_to-infty
by A30, LIMFUNC1:7; verum