let x0 be Real; for f1, f2 being PartFunc of REAL,REAL st f1 is_right_convergent_in x0 & lim_right (f1,x0) = 0 & ( for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom (f1 (#) f2) ) ) & ex r being Real st
( 0 < r & f2 | ].x0,(x0 + r).[ is bounded ) holds
( f1 (#) f2 is_right_convergent_in x0 & lim_right ((f1 (#) f2),x0) = 0 )
let f1, f2 be PartFunc of REAL,REAL; ( f1 is_right_convergent_in x0 & lim_right (f1,x0) = 0 & ( for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom (f1 (#) f2) ) ) & ex r being Real st
( 0 < r & f2 | ].x0,(x0 + r).[ is bounded ) implies ( f1 (#) f2 is_right_convergent_in x0 & lim_right ((f1 (#) f2),x0) = 0 ) )
assume that
A1:
f1 is_right_convergent_in x0
and
A2:
lim_right (f1,x0) = 0
and
A3:
for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom (f1 (#) f2) )
; ( for r being Real holds
( not 0 < r or not f2 | ].x0,(x0 + r).[ is bounded ) or ( f1 (#) f2 is_right_convergent_in x0 & lim_right ((f1 (#) f2),x0) = 0 ) )
given r being Real such that A4:
0 < r
and
A5:
f2 | ].x0,(x0 + r).[ is bounded
; ( f1 (#) f2 is_right_convergent_in x0 & lim_right ((f1 (#) f2),x0) = 0 )
consider g being Real such that
A6:
for r1 being object st r1 in ].x0,(x0 + r).[ /\ (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)) /\ (right_open_halfline x0) holds
( (f1 (#) f2) /* s is convergent & lim ((f1 (#) f2) /* s) = 0 )set L =
right_open_halfline x0;
let s be
Real_Sequence;
( s is convergent & lim s = x0 & rng s c= (dom (f1 (#) f2)) /\ (right_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)) /\ (right_open_halfline x0)
;
( (f1 (#) f2) /* s is convergent & lim ((f1 (#) f2) /* s) = 0 )
x0 < x0 + r
by A4, Lm1;
then consider k being
Nat such that A11:
for
n being
Nat st
k <= n holds
s . n < x0 + r
by A8, A9, Th2;
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) /\ (right_open_halfline x0)
by A10, Lm2;
then A15:
rng (s ^\ k) c= (dom f1) /\ (right_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= right_open_halfline x0
by A10, Lm2;
then A18:
rng (s ^\ k) c= right_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;
s . (n + k) < x0 + r
by A11, NAT_1:12;
then A22:
(s ^\ k) . n < x0 + r
by NAT_1:def 3;
A23:
(s ^\ k) . n in rng (s ^\ k)
by VALUED_0:28;
then
(s ^\ k) . n in right_open_halfline x0
by A18;
then
(s ^\ k) . n in { g1 where g1 is Real : x0 < g1 }
by XXREAL_1:230;
then
ex
g1 being
Real st
(
g1 = (s ^\ k) . n &
x0 < g1 )
;
then
(s ^\ k) . n in { g2 where g2 is Real : ( x0 < g2 & g2 < x0 + r ) }
by A22;
then
(s ^\ k) . n in ].x0,(x0 + r).[
by RCOMP_1:def 2;
then
(s ^\ k) . n in ].x0,(x0 + r).[ /\ (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, Def8;
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_right_convergent_in x0
by A3; lim_right ((f1 (#) f2),x0) = 0
hence
lim_right ((f1 (#) f2),x0) = 0
by A7, Def8; verum