let x0 be Real; for f1, f2 being PartFunc of REAL,REAL st f1 is_left_convergent_in x0 & f2 is_divergent_to-infty_in lim_left (f1,x0) & ( for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom (f2 * f1) ) ) & ex g being Real st
( 0 < g & ( for r being Real st r in (dom f1) /\ ].(x0 - g),x0.[ holds
f1 . r <> lim_left (f1,x0) ) ) holds
f2 * f1 is_left_divergent_to-infty_in x0
let f1, f2 be PartFunc of REAL,REAL; ( f1 is_left_convergent_in x0 & f2 is_divergent_to-infty_in lim_left (f1,x0) & ( for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom (f2 * f1) ) ) & ex g being Real st
( 0 < g & ( for r being Real st r in (dom f1) /\ ].(x0 - g),x0.[ holds
f1 . r <> lim_left (f1,x0) ) ) implies f2 * f1 is_left_divergent_to-infty_in x0 )
assume that
A1:
f1 is_left_convergent_in x0
and
A2:
f2 is_divergent_to-infty_in lim_left (f1,x0)
and
A3:
for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom (f2 * f1) )
; ( for g being Real holds
( not 0 < g or ex r being Real st
( r in (dom f1) /\ ].(x0 - g),x0.[ & not f1 . r <> lim_left (f1,x0) ) ) or f2 * f1 is_left_divergent_to-infty_in x0 )
given g being Real such that A4:
0 < g
and
A5:
for r being Real st r in (dom f1) /\ ].(x0 - g),x0.[ holds
f1 . r <> lim_left (f1,x0)
; f2 * f1 is_left_divergent_to-infty_in x0
now for s being Real_Sequence st s is convergent & lim s = x0 & rng s c= (dom (f2 * f1)) /\ (left_open_halfline x0) holds
(f2 * f1) /* s is divergent_to-infty let s be
Real_Sequence;
( s is convergent & lim s = x0 & rng s c= (dom (f2 * f1)) /\ (left_open_halfline x0) implies (f2 * f1) /* s is divergent_to-infty )assume that A6:
(
s is
convergent &
lim s = x0 )
and A7:
rng s c= (dom (f2 * f1)) /\ (left_open_halfline x0)
;
(f2 * f1) /* s is divergent_to-infty consider k being
Nat such that A8:
for
n being
Nat st
k <= n holds
x0 - g < s . n
by A4, A6, Lm1, LIMFUNC2:1;
set q =
(f1 /* s) ^\ k;
A9:
rng s c= dom (f2 * f1)
by A7, Th1;
rng (f1 /* s) c= dom f2
by A7, Th1;
then A10:
f2 /* ((f1 /* s) ^\ k) =
(f2 /* (f1 /* s)) ^\ k
by VALUED_0:27
.=
((f2 * f1) /* s) ^\ k
by A9, VALUED_0:31
;
A11:
rng s c= (dom f1) /\ (left_open_halfline x0)
by A7, Th1;
then A12:
f1 /* s is
convergent
by A1, A2, A6, LIMFUNC2:def 7;
A13:
rng s c= dom f1
by A7, Th1;
A14:
rng s c= left_open_halfline x0
by A7, Th1;
now for x being object st x in rng ((f1 /* s) ^\ k) holds
x in (dom f2) \ {(lim_left (f1,x0))}let x be
object ;
( x in rng ((f1 /* s) ^\ k) implies x in (dom f2) \ {(lim_left (f1,x0))} )assume
x in rng ((f1 /* s) ^\ k)
;
x in (dom f2) \ {(lim_left (f1,x0))}then consider n being
Element of
NAT such that A15:
((f1 /* s) ^\ k) . n = x
by FUNCT_2:113;
A16:
n + k in NAT
by ORDINAL1:def 12;
A17:
f1 . (s . (n + k)) =
(f1 /* s) . (n + k)
by A13, FUNCT_2:108, A16
.=
x
by A15, NAT_1:def 3
;
A18:
x0 - g < s . (n + k)
by A8, NAT_1:12;
A19:
s . (n + k) in rng s
by VALUED_0:28;
then
s . (n + k) in left_open_halfline x0
by A14;
then
s . (n + k) in { g1 where g1 is Real : g1 < x0 }
by XXREAL_1:229;
then
ex
g1 being
Real st
(
g1 = s . (n + k) &
g1 < x0 )
;
then
s . (n + k) in { g2 where g2 is Real : ( x0 - g < g2 & g2 < x0 ) }
by A18;
then
s . (n + k) in ].(x0 - g),x0.[
by RCOMP_1:def 2;
then
s . (n + k) in (dom f1) /\ ].(x0 - g),x0.[
by A13, A19, XBOOLE_0:def 4;
then
f1 . (s . (n + k)) <> lim_left (
f1,
x0)
by A5;
then A20:
not
f1 . (s . (n + k)) in {(lim_left (f1,x0))}
by TARSKI:def 1;
f1 . (s . (n + k)) in dom f2
by A9, A19, FUNCT_1:11;
hence
x in (dom f2) \ {(lim_left (f1,x0))}
by A20, A17, XBOOLE_0:def 5;
verum end; then A21:
rng ((f1 /* s) ^\ k) c= (dom f2) \ {(lim_left (f1,x0))}
;
lim (f1 /* s) = lim_left (
f1,
x0)
by A1, A6, A11, LIMFUNC2:def 7;
then
lim ((f1 /* s) ^\ k) = lim_left (
f1,
x0)
by A12, SEQ_4:20;
then
f2 /* ((f1 /* s) ^\ k) is
divergent_to-infty
by A2, A12, A21, LIMFUNC3:def 3;
hence
(f2 * f1) /* s is
divergent_to-infty
by A10, LIMFUNC1:7;
verum end;
hence
f2 * f1 is_left_divergent_to-infty_in x0
by A3, LIMFUNC2:def 3; verum