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