let x0 be Real; for f1, f2 being PartFunc of REAL,REAL st f1 is_divergent_to+infty_in x0 & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (f1 (#) f2) & g2 < r2 & x0 < g2 & g2 in dom (f1 (#) f2) ) ) & ex r, r1 being Real st
( 0 < r & 0 < r1 & ( for g being Real st g in (dom f2) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) holds
r1 <= f2 . g ) ) holds
f1 (#) f2 is_divergent_to+infty_in x0
let f1, f2 be PartFunc of REAL,REAL; ( f1 is_divergent_to+infty_in x0 & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (f1 (#) f2) & g2 < r2 & x0 < g2 & g2 in dom (f1 (#) f2) ) ) & ex r, r1 being Real st
( 0 < r & 0 < r1 & ( for g being Real st g in (dom f2) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) holds
r1 <= f2 . g ) ) implies f1 (#) f2 is_divergent_to+infty_in x0 )
assume that
A1:
f1 is_divergent_to+infty_in x0
and
A2:
for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (f1 (#) f2) & g2 < r2 & x0 < g2 & g2 in dom (f1 (#) f2) )
; ( for r, r1 being Real holds
( not 0 < r or not 0 < r1 or ex g being Real st
( g in (dom f2) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) & not r1 <= f2 . g ) ) or f1 (#) f2 is_divergent_to+infty_in x0 )
given r, t being Real such that A3:
0 < r
and
A4:
0 < t
and
A5:
for g being Real st g in (dom f2) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) holds
t <= f2 . g
; f1 (#) f2 is_divergent_to+infty_in x0
now for s being Real_Sequence st s is convergent & lim s = x0 & rng s c= (dom (f1 (#) f2)) \ {x0} holds
(f1 (#) f2) /* s is divergent_to+infty let s be
Real_Sequence;
( s is convergent & lim s = x0 & rng s c= (dom (f1 (#) f2)) \ {x0} implies (f1 (#) f2) /* s is divergent_to+infty )assume that A6:
s is
convergent
and A7:
lim s = x0
and A8:
rng s c= (dom (f1 (#) f2)) \ {x0}
;
(f1 (#) f2) /* s is divergent_to+infty consider k being
Element of
NAT such that A9:
for
n being
Element of
NAT st
k <= n holds
(
x0 - r < s . n &
s . n < x0 + r )
by A3, A6, A7, Th7;
A10:
rng s c= dom (f1 (#) f2)
by A8, Lm2;
A11:
dom (f1 (#) f2) = (dom f1) /\ (dom f2)
by A8, Lm2;
rng (s ^\ k) c= rng s
by VALUED_0:21;
then A12:
rng (s ^\ k) c= (dom (f1 (#) f2)) \ {x0}
by A8;
then A13:
rng (s ^\ k) c= (dom f1) \ {x0}
by Lm2;
A14:
rng (s ^\ k) c= dom f2
by A12, Lm2;
A15:
now ( 0 < t & ( for n being Nat holds t <= (f2 /* (s ^\ k)) . n ) )thus
0 < t
by A4;
for n being Nat holds t <= (f2 /* (s ^\ k)) . nlet n be
Nat;
t <= (f2 /* (s ^\ k)) . nA16:
n in NAT
by ORDINAL1:def 12;
A17:
k <= n + k
by NAT_1:12;
then
s . (n + k) < x0 + r
by A9;
then A18:
(s ^\ k) . n < x0 + r
by NAT_1:def 3;
x0 - r < s . (n + k)
by A9, A17;
then
x0 - r < (s ^\ k) . n
by NAT_1:def 3;
then
(s ^\ k) . n in { g2 where g2 is Real : ( x0 - r < g2 & g2 < x0 + r ) }
by A18;
then A19:
(s ^\ k) . n in ].(x0 - r),(x0 + r).[
by RCOMP_1:def 2;
A20:
(s ^\ k) . n in rng (s ^\ k)
by VALUED_0:28;
then
not
(s ^\ k) . n in {x0}
by A12, XBOOLE_0:def 5;
then
(s ^\ k) . n in ].(x0 - r),(x0 + r).[ \ {x0}
by A19, XBOOLE_0:def 5;
then
(s ^\ k) . n in ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[
by A3, Th4;
then
(s ^\ k) . n in (dom f2) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[)
by A14, A20, XBOOLE_0:def 4;
then
t <= f2 . ((s ^\ k) . n)
by A5;
hence
t <= (f2 /* (s ^\ k)) . n
by A14, FUNCT_2:108, A16;
verum end;
lim (s ^\ k) = x0
by A6, A7, SEQ_4:20;
then
f1 /* (s ^\ k) is
divergent_to+infty
by A1, A6, A13;
then A21:
(f1 /* (s ^\ k)) (#) (f2 /* (s ^\ k)) is
divergent_to+infty
by A15, LIMFUNC1:22;
rng (s ^\ k) c= dom (f1 (#) f2)
by A12, Lm2;
then (f1 /* (s ^\ k)) (#) (f2 /* (s ^\ k)) =
(f1 (#) f2) /* (s ^\ k)
by A11, RFUNCT_2:8
.=
((f1 (#) f2) /* s) ^\ k
by A10, VALUED_0:27
;
hence
(f1 (#) f2) /* s is
divergent_to+infty
by A21, LIMFUNC1:7;
verum end;
hence
f1 (#) f2 is_divergent_to+infty_in x0
by A2; verum