let x0 be Real; for f being PartFunc of REAL,REAL st f is_convergent_in x0 & lim (f,x0) = 0 & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f & f . g1 <> 0 & f . g2 <> 0 ) ) & ex r being Real st
( 0 < r & ( for g being Real st g in (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) holds
0 <= f . g ) ) holds
f ^ is_divergent_to+infty_in x0
let f be PartFunc of REAL,REAL; ( f is_convergent_in x0 & lim (f,x0) = 0 & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f & f . g1 <> 0 & f . g2 <> 0 ) ) & ex r being Real st
( 0 < r & ( for g being Real st g in (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) holds
0 <= f . g ) ) implies f ^ is_divergent_to+infty_in x0 )
assume that
A1:
f is_convergent_in x0
and
A2:
lim (f,x0) = 0
and
A3:
for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f & f . g1 <> 0 & f . g2 <> 0 )
; ( for r being Real holds
( not 0 < r or ex g being Real st
( g in (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) & not 0 <= f . g ) ) or f ^ is_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 - r),x0.[ \/ ].x0,(x0 + r).[) holds
0 <= f . g
; f ^ is_divergent_to+infty_in x0
thus
for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (f ^) & g2 < r2 & x0 < g2 & g2 in dom (f ^) )
LIMFUNC3:def 2 for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom (f ^)) \ {x0} holds
(f ^) /* seq is divergent_to+infty proof
let r1,
r2 be
Real;
( r1 < x0 & x0 < r2 implies ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (f ^) & g2 < r2 & x0 < g2 & g2 in dom (f ^) ) )
assume that A6:
r1 < x0
and A7:
x0 < r2
;
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (f ^) & g2 < r2 & x0 < g2 & g2 in dom (f ^) )
consider g1,
g2 being
Real such that A8:
r1 < g1
and A9:
g1 < x0
and A10:
g1 in dom f
and A11:
g2 < r2
and A12:
x0 < g2
and A13:
g2 in dom f
and A14:
f . g1 <> 0
and A15:
f . g2 <> 0
by A3, A6, A7;
not
f . g2 in {0}
by A15, TARSKI:def 1;
then
not
g2 in f " {0}
by FUNCT_1:def 7;
then A16:
g2 in (dom f) \ (f " {0})
by A13, XBOOLE_0:def 5;
take
g1
;
ex g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (f ^) & g2 < r2 & x0 < g2 & g2 in dom (f ^) )
take
g2
;
( r1 < g1 & g1 < x0 & g1 in dom (f ^) & g2 < r2 & x0 < g2 & g2 in dom (f ^) )
not
f . g1 in {0}
by A14, TARSKI:def 1;
then
not
g1 in f " {0}
by FUNCT_1:def 7;
then
g1 in (dom f) \ (f " {0})
by A10, XBOOLE_0:def 5;
hence
(
r1 < g1 &
g1 < x0 &
g1 in dom (f ^) &
g2 < r2 &
x0 < g2 &
g2 in dom (f ^) )
by A8, A9, A11, A12, A16, RFUNCT_1:def 2;
verum
end;
let s be Real_Sequence; ( s is convergent & lim s = x0 & rng s c= (dom (f ^)) \ {x0} implies (f ^) /* s is divergent_to+infty )
assume that
A17:
s is convergent
and
A18:
lim s = x0
and
A19:
rng s c= (dom (f ^)) \ {x0}
; (f ^) /* s is divergent_to+infty
consider k being Element of NAT such that
A20:
for n being Element of NAT st k <= n holds
( x0 - r < s . n & s . n < x0 + r )
by A4, A17, A18, Th7;
A21:
rng s c= dom (f ^)
by A19, XBOOLE_1:1;
A22:
dom (f ^) = (dom f) \ (f " {0})
by RFUNCT_1:def 2;
then A23: (f /* (s ^\ k)) " =
((f /* s) ^\ k) "
by A21, VALUED_0:27, XBOOLE_1:1
.=
((f /* s) ") ^\ k
by SEQM_3:18
.=
((f ^) /* s) ^\ k
by A19, RFUNCT_2:12, XBOOLE_1:1
;
A24:
rng (s ^\ k) c= rng s
by VALUED_0:21;
A25:
rng s c= dom f
by A21, A22, XBOOLE_1:1;
then A26:
rng (s ^\ k) c= dom f
by A24;
A27:
rng (s ^\ k) c= (dom (f ^)) \ {x0}
by A19, A24;
A28:
rng (s ^\ k) c= (dom f) \ {x0}
A30:
lim (s ^\ k) = x0
by A17, A18, SEQ_4:20;
then A31:
lim (f /* (s ^\ k)) = 0
by A1, A2, A17, A28, Def4;
A32:
f /* (s ^\ k) is non-zero
by A21, A24, RFUNCT_2:11, XBOOLE_1:1;
now for n being Nat holds 0 < (f /* (s ^\ k)) . nlet n be
Nat;
0 < (f /* (s ^\ k)) . nA33:
n in NAT
by ORDINAL1:def 12;
A34:
k <= n + k
by NAT_1:12;
then
s . (n + k) < x0 + r
by A20;
then A35:
(s ^\ k) . n < x0 + r
by NAT_1:def 3;
x0 - r < s . (n + k)
by A20, A34;
then
x0 - r < (s ^\ k) . n
by NAT_1:def 3;
then
(s ^\ k) . n in { g1 where g1 is Real : ( x0 - r < g1 & g1 < x0 + r ) }
by A35;
then A36:
(s ^\ k) . n in ].(x0 - r),(x0 + r).[
by RCOMP_1:def 2;
A37:
(s ^\ k) . n in rng (s ^\ k)
by VALUED_0:28;
then
not
(s ^\ k) . n in {x0}
by A27, XBOOLE_0:def 5;
then
(s ^\ k) . n in ].(x0 - r),(x0 + r).[ \ {x0}
by A36, XBOOLE_0:def 5;
then
(s ^\ k) . n in ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[
by A4, Th4;
then
(s ^\ k) . n in (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[)
by A26, A37, XBOOLE_0:def 4;
then A38:
0 <= f . ((s ^\ k) . n)
by A5;
(f /* (s ^\ k)) . n <> 0
by A32, SEQ_1:5;
hence
0 < (f /* (s ^\ k)) . n
by A25, A24, A38, FUNCT_2:108, XBOOLE_1:1, A33;
verum end;
then A39:
for n being Nat st 0 <= n holds
0 < (f /* (s ^\ k)) . n
;
f /* (s ^\ k) is convergent
by A1, A17, A30, A28;
then
(f /* (s ^\ k)) " is divergent_to+infty
by A31, A39, LIMFUNC1:35;
hence
(f ^) /* s is divergent_to+infty
by A23, LIMFUNC1:7; verum