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