let x0 be Real; for f, f1, f2 being PartFunc of REAL,REAL st f1 is_convergent_in x0 & f2 is_convergent_in x0 & lim (f1,x0) = lim (f2,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 f & g2 < r2 & x0 < g2 & g2 in dom f ) ) & ex r being Real st
( 0 < r & ( for g being Real st g in (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) holds
( f1 . g <= f . g & f . g <= f2 . g ) ) & ( ( (dom f1) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) c= (dom f2) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) & (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) c= (dom f1) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) ) or ( (dom f2) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) c= (dom f1) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) & (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) c= (dom f2) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) ) ) ) holds
( f is_convergent_in x0 & lim (f,x0) = lim (f1,x0) )
let f, f1, f2 be PartFunc of REAL,REAL; ( f1 is_convergent_in x0 & f2 is_convergent_in x0 & lim (f1,x0) = lim (f2,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 f & g2 < r2 & x0 < g2 & g2 in dom f ) ) & ex r being Real st
( 0 < r & ( for g being Real st g in (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) holds
( f1 . g <= f . g & f . g <= f2 . g ) ) & ( ( (dom f1) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) c= (dom f2) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) & (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) c= (dom f1) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) ) or ( (dom f2) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) c= (dom f1) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) & (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) c= (dom f2) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) ) ) ) implies ( f is_convergent_in x0 & lim (f,x0) = lim (f1,x0) ) )
assume that
A1:
f1 is_convergent_in x0
and
A2:
f2 is_convergent_in x0
and
A3:
lim (f1,x0) = lim (f2,x0)
and
A4:
for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f )
; ( for r being Real holds
( not 0 < r or ex g being Real st
( g in (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) & not ( f1 . g <= f . g & f . g <= f2 . g ) ) or ( not ( (dom f1) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) c= (dom f2) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) & (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) c= (dom f1) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) ) & not ( (dom f2) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) c= (dom f1) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) & (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) c= (dom f2) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) ) ) ) or ( f is_convergent_in x0 & lim (f,x0) = lim (f1,x0) ) )
given r1 being Real such that A5:
0 < r1
and
A6:
for g being Real st g in (dom f) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[) holds
( f1 . g <= f . g & f . g <= f2 . g )
and
A7:
( ( (dom f1) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[) c= (dom f2) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[) & (dom f) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[) c= (dom f1) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[) ) or ( (dom f2) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[) c= (dom f1) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[) & (dom f) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[) c= (dom f2) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[) ) )
; ( f is_convergent_in x0 & lim (f,x0) = lim (f1,x0) )
now ( f is_convergent_in x0 & f is_convergent_in x0 & lim (f,x0) = lim (f1,x0) )per cases
( ( (dom f1) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[) c= (dom f2) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[) & (dom f) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[) c= (dom f1) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[) ) or ( (dom f2) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[) c= (dom f1) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[) & (dom f) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[) c= (dom f2) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[) ) )
by A7;
suppose A8:
(
(dom f1) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[) c= (dom f2) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[) &
(dom f) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[) c= (dom f1) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[) )
;
( f is_convergent_in x0 & f is_convergent_in x0 & lim (f,x0) = lim (f1,x0) )A9:
now for s being Real_Sequence st s is convergent & lim s = x0 & rng s c= (dom f) \ {x0} holds
( f /* s is convergent & lim (f /* s) = lim (f1,x0) )let s be
Real_Sequence;
( s is convergent & lim s = x0 & rng s c= (dom f) \ {x0} implies ( f /* s is convergent & lim (f /* s) = lim (f1,x0) ) )assume that A10:
s is
convergent
and A11:
lim s = x0
and A12:
rng s c= (dom f) \ {x0}
;
( f /* s is convergent & lim (f /* s) = lim (f1,x0) )consider k being
Element of
NAT such that A13:
for
n being
Element of
NAT st
k <= n holds
(
x0 - r1 < s . n &
s . n < x0 + r1 )
by A5, A10, A11, Th7;
A14:
rng (s ^\ k) c= rng s
by VALUED_0:21;
then A15:
rng (s ^\ k) c= (dom f) \ {x0}
by A12;
now for x being object st x in rng (s ^\ k) holds
x in ].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[let x be
object ;
( x in rng (s ^\ k) implies x in ].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[ )assume A16:
x in rng (s ^\ k)
;
x in ].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[then consider n being
Element of
NAT such that A17:
x = (s ^\ k) . n
by FUNCT_2:113;
A18:
k <= n + k
by NAT_1:12;
then
s . (n + k) < x0 + r1
by A13;
then A19:
(s ^\ k) . n < x0 + r1
by NAT_1:def 3;
x0 - r1 < s . (n + k)
by A13, A18;
then
x0 - r1 < (s ^\ k) . n
by NAT_1:def 3;
then
(s ^\ k) . n in { g1 where g1 is Real : ( x0 - r1 < g1 & g1 < x0 + r1 ) }
by A19;
then A20:
(s ^\ k) . n in ].(x0 - r1),(x0 + r1).[
by RCOMP_1:def 2;
not
(s ^\ k) . n in {x0}
by A15, A16, A17, XBOOLE_0:def 5;
then
x in ].(x0 - r1),(x0 + r1).[ \ {x0}
by A17, A20, XBOOLE_0:def 5;
hence
x in ].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[
by A5, Th4;
verum end; then A21:
rng (s ^\ k) c= ].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[
;
A22:
rng s c= dom f
by A12, XBOOLE_1:1;
then
rng (s ^\ k) c= dom f
by A14;
then A23:
rng (s ^\ k) c= (dom f) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[)
by A21, XBOOLE_1:19;
then A24:
rng (s ^\ k) c= (dom f1) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[)
by A8;
then A25:
rng (s ^\ k) c= (dom f2) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[)
by A8;
A26:
lim (s ^\ k) = x0
by A10, A11, SEQ_4:20;
A27:
(dom f2) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[) c= dom f2
by XBOOLE_1:17;
then A28:
rng (s ^\ k) c= dom f2
by A25;
A29:
rng (s ^\ k) c= (dom f2) \ {x0}
then A31:
lim (f2 /* (s ^\ k)) = lim (
f2,
x0)
by A2, A10, A26, Def4;
A32:
(dom f1) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[) c= dom f1
by XBOOLE_1:17;
then A33:
rng (s ^\ k) c= dom f1
by A24;
A34:
rng (s ^\ k) c= (dom f1) \ {x0}
then A36:
lim (f1 /* (s ^\ k)) = lim (
f1,
x0)
by A1, A10, A26, Def4;
A37:
now for n being Nat holds
( (f1 /* (s ^\ k)) . n <= (f /* (s ^\ k)) . n & (f /* (s ^\ k)) . n <= (f2 /* (s ^\ k)) . n )let n be
Nat;
( (f1 /* (s ^\ k)) . n <= (f /* (s ^\ k)) . n & (f /* (s ^\ k)) . n <= (f2 /* (s ^\ k)) . n )A38:
n in NAT
by ORDINAL1:def 12;
A39:
(s ^\ k) . n in rng (s ^\ k)
by VALUED_0:28;
then
f . ((s ^\ k) . n) <= f2 . ((s ^\ k) . n)
by A6, A23;
then A40:
(f /* (s ^\ k)) . n <= f2 . ((s ^\ k) . n)
by A14, A22, FUNCT_2:108, XBOOLE_1:1, A38;
f1 . ((s ^\ k) . n) <= f . ((s ^\ k) . n)
by A6, A23, A39;
then
f1 . ((s ^\ k) . n) <= (f /* (s ^\ k)) . n
by A14, A22, FUNCT_2:108, XBOOLE_1:1, A38;
hence
(
(f1 /* (s ^\ k)) . n <= (f /* (s ^\ k)) . n &
(f /* (s ^\ k)) . n <= (f2 /* (s ^\ k)) . n )
by A32, A27, A24, A25, A40, FUNCT_2:108, XBOOLE_1:1, A38;
verum end; A41:
f2 /* (s ^\ k) is
convergent
by A2, A10, A26, A29;
A42:
f1 /* (s ^\ k) is
convergent
by A1, A10, A26, A34;
then
f /* (s ^\ k) is
convergent
by A3, A36, A41, A31, A37, SEQ_2:19;
then A43:
(f /* s) ^\ k is
convergent
by A12, VALUED_0:27, XBOOLE_1:1;
hence
f /* s is
convergent
by SEQ_4:21;
lim (f /* s) = lim (f1,x0)
lim (f /* (s ^\ k)) = lim (
f1,
x0)
by A3, A42, A36, A41, A31, A37, SEQ_2:20;
then
lim ((f /* s) ^\ k) = lim (
f1,
x0)
by A12, VALUED_0:27, XBOOLE_1:1;
hence
lim (f /* s) = lim (
f1,
x0)
by A43, SEQ_4:22;
verum end; hence
f is_convergent_in x0
by A4;
( f is_convergent_in x0 & lim (f,x0) = lim (f1,x0) )hence
(
f is_convergent_in x0 &
lim (
f,
x0)
= lim (
f1,
x0) )
by A9, Def4;
verum suppose A44:
(
(dom f2) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[) c= (dom f1) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[) &
(dom f) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[) c= (dom f2) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[) )
;
( f is_convergent_in x0 & f is_convergent_in x0 & lim (f,x0) = lim (f1,x0) )A45:
now for s being Real_Sequence st s is convergent & lim s = x0 & rng s c= (dom f) \ {x0} holds
( f /* s is convergent & lim (f /* s) = lim (f1,x0) )let s be
Real_Sequence;
( s is convergent & lim s = x0 & rng s c= (dom f) \ {x0} implies ( f /* s is convergent & lim (f /* s) = lim (f1,x0) ) )assume that A46:
s is
convergent
and A47:
lim s = x0
and A48:
rng s c= (dom f) \ {x0}
;
( f /* s is convergent & lim (f /* s) = lim (f1,x0) )consider k being
Element of
NAT such that A49:
for
n being
Element of
NAT st
k <= n holds
(
x0 - r1 < s . n &
s . n < x0 + r1 )
by A5, A46, A47, Th7;
A50:
rng (s ^\ k) c= rng s
by VALUED_0:21;
then A51:
rng (s ^\ k) c= (dom f) \ {x0}
by A48;
now for x being object st x in rng (s ^\ k) holds
x in ].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[let x be
object ;
( x in rng (s ^\ k) implies x in ].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[ )assume A52:
x in rng (s ^\ k)
;
x in ].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[then consider n being
Element of
NAT such that A53:
x = (s ^\ k) . n
by FUNCT_2:113;
A54:
k <= n + k
by NAT_1:12;
then
s . (n + k) < x0 + r1
by A49;
then A55:
(s ^\ k) . n < x0 + r1
by NAT_1:def 3;
x0 - r1 < s . (n + k)
by A49, A54;
then
x0 - r1 < (s ^\ k) . n
by NAT_1:def 3;
then
(s ^\ k) . n in { g1 where g1 is Real : ( x0 - r1 < g1 & g1 < x0 + r1 ) }
by A55;
then A56:
(s ^\ k) . n in ].(x0 - r1),(x0 + r1).[
by RCOMP_1:def 2;
not
(s ^\ k) . n in {x0}
by A51, A52, A53, XBOOLE_0:def 5;
then
x in ].(x0 - r1),(x0 + r1).[ \ {x0}
by A53, A56, XBOOLE_0:def 5;
hence
x in ].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[
by A5, Th4;
verum end; then A57:
rng (s ^\ k) c= ].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[
;
A58:
rng s c= dom f
by A48, XBOOLE_1:1;
then
rng (s ^\ k) c= dom f
by A50;
then A59:
rng (s ^\ k) c= (dom f) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[)
by A57, XBOOLE_1:19;
then A60:
rng (s ^\ k) c= (dom f2) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[)
by A44;
then A61:
rng (s ^\ k) c= (dom f1) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[)
by A44;
A62:
lim (s ^\ k) = x0
by A46, A47, SEQ_4:20;
A63:
(dom f2) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[) c= dom f2
by XBOOLE_1:17;
then A64:
rng (s ^\ k) c= dom f2
by A60;
A65:
rng (s ^\ k) c= (dom f2) \ {x0}
then A67:
lim (f2 /* (s ^\ k)) = lim (
f2,
x0)
by A2, A46, A62, Def4;
A68:
(dom f1) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[) c= dom f1
by XBOOLE_1:17;
then A69:
rng (s ^\ k) c= dom f1
by A61;
A70:
rng (s ^\ k) c= (dom f1) \ {x0}
then A72:
lim (f1 /* (s ^\ k)) = lim (
f1,
x0)
by A1, A46, A62, Def4;
A73:
now for n being Nat holds
( (f1 /* (s ^\ k)) . n <= (f /* (s ^\ k)) . n & (f /* (s ^\ k)) . n <= (f2 /* (s ^\ k)) . n )let n be
Nat;
( (f1 /* (s ^\ k)) . n <= (f /* (s ^\ k)) . n & (f /* (s ^\ k)) . n <= (f2 /* (s ^\ k)) . n )A74:
n in NAT
by ORDINAL1:def 12;
A75:
(s ^\ k) . n in rng (s ^\ k)
by VALUED_0:28;
then
f . ((s ^\ k) . n) <= f2 . ((s ^\ k) . n)
by A6, A59;
then A76:
(f /* (s ^\ k)) . n <= f2 . ((s ^\ k) . n)
by A50, A58, FUNCT_2:108, XBOOLE_1:1, A74;
f1 . ((s ^\ k) . n) <= f . ((s ^\ k) . n)
by A6, A59, A75;
then
f1 . ((s ^\ k) . n) <= (f /* (s ^\ k)) . n
by A50, A58, FUNCT_2:108, XBOOLE_1:1, A74;
hence
(
(f1 /* (s ^\ k)) . n <= (f /* (s ^\ k)) . n &
(f /* (s ^\ k)) . n <= (f2 /* (s ^\ k)) . n )
by A68, A63, A60, A61, A76, FUNCT_2:108, XBOOLE_1:1, A74;
verum end; A77:
f2 /* (s ^\ k) is
convergent
by A2, A46, A62, A65;
A78:
f1 /* (s ^\ k) is
convergent
by A1, A46, A62, A70;
then
f /* (s ^\ k) is
convergent
by A3, A72, A77, A67, A73, SEQ_2:19;
then A79:
(f /* s) ^\ k is
convergent
by A48, VALUED_0:27, XBOOLE_1:1;
hence
f /* s is
convergent
by SEQ_4:21;
lim (f /* s) = lim (f1,x0)
lim (f /* (s ^\ k)) = lim (
f1,
x0)
by A3, A78, A72, A77, A67, A73, SEQ_2:20;
then
lim ((f /* s) ^\ k) = lim (
f1,
x0)
by A48, VALUED_0:27, XBOOLE_1:1;
hence
lim (f /* s) = lim (
f1,
x0)
by A79, SEQ_4:22;
verum end; hence
f is_convergent_in x0
by A4;
( f is_convergent_in x0 & lim (f,x0) = lim (f1,x0) )hence
(
f is_convergent_in x0 &
lim (
f,
x0)
= lim (
f1,
x0) )
by A45, Def4;
verum
hence
( f is_convergent_in x0 & lim (f,x0) = lim (f1,x0) )
; verum