let x0 be Real; for f1, f2 being PartFunc of REAL,REAL st f1 is_left_convergent_in x0 & lim_left (f1,x0) = 0 & ( for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom (f1 (#) f2) ) ) & ex r being Real st
( 0 < r & f2 | ].(x0 - r),x0.[ is bounded ) holds
( f1 (#) f2 is_left_convergent_in x0 & lim_left ((f1 (#) f2),x0) = 0 )
let f1, f2 be PartFunc of REAL,REAL; ( f1 is_left_convergent_in x0 & lim_left (f1,x0) = 0 & ( for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom (f1 (#) f2) ) ) & ex r being Real st
( 0 < r & f2 | ].(x0 - r),x0.[ is bounded ) implies ( f1 (#) f2 is_left_convergent_in x0 & lim_left ((f1 (#) f2),x0) = 0 ) )
assume that
A1:
f1 is_left_convergent_in x0
and
A2:
lim_left (f1,x0) = 0
and
A3:
for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom (f1 (#) f2) )
; ( for r being Real holds
( not 0 < r or not f2 | ].(x0 - r),x0.[ is bounded ) or ( f1 (#) f2 is_left_convergent_in x0 & lim_left ((f1 (#) f2),x0) = 0 ) )
given r being Real such that A4:
0 < r
and
A5:
f2 | ].(x0 - r),x0.[ is bounded
; ( f1 (#) f2 is_left_convergent_in x0 & lim_left ((f1 (#) f2),x0) = 0 )
consider g being Real such that
A6:
for r1 being object st r1 in ].(x0 - r),x0.[ /\ (dom f2) holds
|.(f2 . r1).| <= g
by A5, RFUNCT_1:73;
A7:
now for s being Real_Sequence st s is convergent & lim s = x0 & rng s c= (dom (f1 (#) f2)) /\ (left_open_halfline x0) holds
( (f1 (#) f2) /* s is convergent & lim ((f1 (#) f2) /* s) = 0 )set L =
left_open_halfline x0;
let s be
Real_Sequence;
( s is convergent & lim s = x0 & rng s c= (dom (f1 (#) f2)) /\ (left_open_halfline x0) implies ( (f1 (#) f2) /* s is convergent & lim ((f1 (#) f2) /* s) = 0 ) )assume that A8:
s is
convergent
and A9:
lim s = x0
and A10:
rng s c= (dom (f1 (#) f2)) /\ (left_open_halfline x0)
;
( (f1 (#) f2) /* s is convergent & lim ((f1 (#) f2) /* s) = 0 )
x0 - r < x0
by A4, Lm1;
then consider k being
Nat such that A11:
for
n being
Nat st
k <= n holds
x0 - r < s . n
by A8, A9, Th1;
A12:
rng (s ^\ k) c= rng s
by VALUED_0:21;
A13:
rng s c= dom (f1 (#) f2)
by A10, Lm2;
dom (f1 (#) f2) = (dom f1) /\ (dom f2)
by A10, Lm2;
then
rng (s ^\ k) c= (dom f1) /\ (dom f2)
by A13, A12, XBOOLE_1:1;
then A14:
(f1 /* (s ^\ k)) (#) (f2 /* (s ^\ k)) =
(f1 (#) f2) /* (s ^\ k)
by RFUNCT_2:8
.=
((f1 (#) f2) /* s) ^\ k
by A13, VALUED_0:27
;
rng s c= (dom f1) /\ (left_open_halfline x0)
by A10, Lm2;
then A15:
rng (s ^\ k) c= (dom f1) /\ (left_open_halfline x0)
by A12, XBOOLE_1:1;
A16:
lim (s ^\ k) = x0
by A8, A9, SEQ_4:20;
then A17:
f1 /* (s ^\ k) is
convergent
by A1, A8, A15;
rng s c= left_open_halfline x0
by A10, Lm2;
then A18:
rng (s ^\ k) c= left_open_halfline x0
by A12, XBOOLE_1:1;
A19:
rng s c= dom f2
by A10, Lm2;
then A20:
rng (s ^\ k) c= dom f2
by A12, XBOOLE_1:1;
now ( 0 < |.g.| + 1 & ( for n being Nat holds |.((f2 /* (s ^\ k)) . n).| < |.g.| + 1 ) )set t =
|.g.| + 1;
0 <= |.g.|
by COMPLEX1:46;
hence
0 < |.g.| + 1
;
for n being Nat holds |.((f2 /* (s ^\ k)) . n).| < |.g.| + 1let n be
Nat;
|.((f2 /* (s ^\ k)) . n).| < |.g.| + 1A21:
n in NAT
by ORDINAL1:def 12;
x0 - r < s . (n + k)
by A11, NAT_1:12;
then A22:
x0 - r < (s ^\ k) . n
by NAT_1:def 3;
A23:
(s ^\ k) . n in rng (s ^\ k)
by VALUED_0:28;
then
(s ^\ k) . n in left_open_halfline x0
by A18;
then
(s ^\ k) . n in { g1 where g1 is Real : g1 < x0 }
by XXREAL_1:229;
then
ex
g1 being
Real st
(
g1 = (s ^\ k) . n &
g1 < x0 )
;
then
(s ^\ k) . n in { g2 where g2 is Real : ( x0 - r < g2 & g2 < x0 ) }
by A22;
then
(s ^\ k) . n in ].(x0 - r),x0.[
by RCOMP_1:def 2;
then
(s ^\ k) . n in ].(x0 - r),x0.[ /\ (dom f2)
by A20, A23, XBOOLE_0:def 4;
then
|.(f2 . ((s ^\ k) . n)).| <= g
by A6;
then A24:
|.((f2 /* (s ^\ k)) . n).| <= g
by A19, A12, FUNCT_2:108, XBOOLE_1:1, A21;
g <= |.g.|
by ABSVALUE:4;
then
g < |.g.| + 1
by Lm1;
hence
|.((f2 /* (s ^\ k)) . n).| < |.g.| + 1
by A24, XXREAL_0:2;
verum end; then A25:
f2 /* (s ^\ k) is
bounded
by SEQ_2:3;
A26:
lim (f1 /* (s ^\ k)) = 0
by A1, A2, A8, A16, A15, Def7;
then A27:
(f1 /* (s ^\ k)) (#) (f2 /* (s ^\ k)) is
convergent
by A17, A25, SEQ_2:25;
hence
(f1 (#) f2) /* s is
convergent
by A14, SEQ_4:21;
lim ((f1 (#) f2) /* s) = 0
lim ((f1 /* (s ^\ k)) (#) (f2 /* (s ^\ k))) = 0
by A17, A26, A25, SEQ_2:26;
hence
lim ((f1 (#) f2) /* s) = 0
by A27, A14, SEQ_4:22;
verum end;
hence
f1 (#) f2 is_left_convergent_in x0
by A3; lim_left ((f1 (#) f2),x0) = 0
hence
lim_left ((f1 (#) f2),x0) = 0
by A7, Def7; verum