let x0 be Real; for f, f1, f2 being PartFunc of REAL,REAL st f1 is_right_convergent_in x0 & f2 is_right_convergent_in x0 & lim_right (f1,x0) = lim_right (f2,x0) & ( for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom f ) ) & ex r being Real st
( 0 < r & ( for g being Real st g in (dom f) /\ ].x0,(x0 + r).[ holds
( f1 . g <= f . g & f . g <= f2 . g ) ) & ( ( (dom f1) /\ ].x0,(x0 + r).[ c= (dom f2) /\ ].x0,(x0 + r).[ & (dom f) /\ ].x0,(x0 + r).[ c= (dom f1) /\ ].x0,(x0 + r).[ ) or ( (dom f2) /\ ].x0,(x0 + r).[ c= (dom f1) /\ ].x0,(x0 + r).[ & (dom f) /\ ].x0,(x0 + r).[ c= (dom f2) /\ ].x0,(x0 + r).[ ) ) ) holds
( f is_right_convergent_in x0 & lim_right (f,x0) = lim_right (f1,x0) )
let f, f1, f2 be PartFunc of REAL,REAL; ( f1 is_right_convergent_in x0 & f2 is_right_convergent_in x0 & lim_right (f1,x0) = lim_right (f2,x0) & ( for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom f ) ) & ex r being Real st
( 0 < r & ( for g being Real st g in (dom f) /\ ].x0,(x0 + r).[ holds
( f1 . g <= f . g & f . g <= f2 . g ) ) & ( ( (dom f1) /\ ].x0,(x0 + r).[ c= (dom f2) /\ ].x0,(x0 + r).[ & (dom f) /\ ].x0,(x0 + r).[ c= (dom f1) /\ ].x0,(x0 + r).[ ) or ( (dom f2) /\ ].x0,(x0 + r).[ c= (dom f1) /\ ].x0,(x0 + r).[ & (dom f) /\ ].x0,(x0 + r).[ c= (dom f2) /\ ].x0,(x0 + r).[ ) ) ) implies ( f is_right_convergent_in x0 & lim_right (f,x0) = lim_right (f1,x0) ) )
assume that
A1:
f1 is_right_convergent_in x0
and
A2:
f2 is_right_convergent_in x0
and
A3:
lim_right (f1,x0) = lim_right (f2,x0)
and
A4:
for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom f )
; ( for r being Real holds
( not 0 < r or ex g being Real st
( g in (dom f) /\ ].x0,(x0 + r).[ & not ( f1 . g <= f . g & f . g <= f2 . g ) ) or ( not ( (dom f1) /\ ].x0,(x0 + r).[ c= (dom f2) /\ ].x0,(x0 + r).[ & (dom f) /\ ].x0,(x0 + r).[ c= (dom f1) /\ ].x0,(x0 + r).[ ) & not ( (dom f2) /\ ].x0,(x0 + r).[ c= (dom f1) /\ ].x0,(x0 + r).[ & (dom f) /\ ].x0,(x0 + r).[ c= (dom f2) /\ ].x0,(x0 + r).[ ) ) ) or ( f is_right_convergent_in x0 & lim_right (f,x0) = lim_right (f1,x0) ) )
given r1 being Real such that A5:
0 < r1
and
A6:
for g being Real st g in (dom f) /\ ].x0,(x0 + r1).[ holds
( f1 . g <= f . g & f . g <= f2 . g )
and
A7:
( ( (dom f1) /\ ].x0,(x0 + r1).[ c= (dom f2) /\ ].x0,(x0 + r1).[ & (dom f) /\ ].x0,(x0 + r1).[ c= (dom f1) /\ ].x0,(x0 + r1).[ ) or ( (dom f2) /\ ].x0,(x0 + r1).[ c= (dom f1) /\ ].x0,(x0 + r1).[ & (dom f) /\ ].x0,(x0 + r1).[ c= (dom f2) /\ ].x0,(x0 + r1).[ ) )
; ( f is_right_convergent_in x0 & lim_right (f,x0) = lim_right (f1,x0) )
now ( f is_right_convergent_in x0 & f is_right_convergent_in x0 & lim_right (f,x0) = lim_right (f1,x0) )per cases
( ( (dom f1) /\ ].x0,(x0 + r1).[ c= (dom f2) /\ ].x0,(x0 + r1).[ & (dom f) /\ ].x0,(x0 + r1).[ c= (dom f1) /\ ].x0,(x0 + r1).[ ) or ( (dom f2) /\ ].x0,(x0 + r1).[ c= (dom f1) /\ ].x0,(x0 + r1).[ & (dom f) /\ ].x0,(x0 + r1).[ c= (dom f2) /\ ].x0,(x0 + r1).[ ) )
by A7;
suppose A8:
(
(dom f1) /\ ].x0,(x0 + r1).[ c= (dom f2) /\ ].x0,(x0 + r1).[ &
(dom f) /\ ].x0,(x0 + r1).[ c= (dom f1) /\ ].x0,(x0 + r1).[ )
;
( f is_right_convergent_in x0 & f is_right_convergent_in x0 & lim_right (f,x0) = lim_right (f1,x0) )A9:
now for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (right_open_halfline x0) holds
( f /* seq is convergent & lim (f /* seq) = lim_right (f1,x0) )let seq be
Real_Sequence;
( seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (right_open_halfline x0) implies ( f /* seq is convergent & lim (f /* seq) = lim_right (f1,x0) ) )assume that A10:
seq is
convergent
and A11:
lim seq = x0
and A12:
rng seq c= (dom f) /\ (right_open_halfline x0)
;
( f /* seq is convergent & lim (f /* seq) = lim_right (f1,x0) )
x0 < (lim seq) + r1
by A5, A11, Lm1;
then consider k being
Nat such that A13:
for
n being
Nat st
k <= n holds
seq . n < x0 + r1
by A10, A11, Th2;
A14:
rng (seq ^\ k) c= rng seq
by VALUED_0:21;
(dom f) /\ (right_open_halfline x0) c= right_open_halfline x0
by XBOOLE_1:17;
then
rng seq c= right_open_halfline x0
by A12, XBOOLE_1:1;
then A15:
rng (seq ^\ k) c= right_open_halfline x0
by A14, XBOOLE_1:1;
then A19:
rng (seq ^\ k) c= ].x0,(x0 + r1).[
by TARSKI:def 3;
].x0,(x0 + r1).[ c= right_open_halfline x0
by XXREAL_1:247;
then A20:
rng (seq ^\ k) c= right_open_halfline x0
by A19, XBOOLE_1:1;
A21:
(dom f) /\ (right_open_halfline x0) c= dom f
by XBOOLE_1:17;
then A22:
rng seq c= dom f
by A12, XBOOLE_1:1;
then
rng (seq ^\ k) c= dom f
by A14, XBOOLE_1:1;
then A23:
rng (seq ^\ k) c= (dom f) /\ ].x0,(x0 + r1).[
by A19, XBOOLE_1:19;
then A24:
rng (seq ^\ k) c= (dom f1) /\ ].x0,(x0 + r1).[
by A8, XBOOLE_1:1;
then A25:
rng (seq ^\ k) c= (dom f2) /\ ].x0,(x0 + r1).[
by A8, XBOOLE_1:1;
A26:
lim (seq ^\ k) = x0
by A10, A11, SEQ_4:20;
A27:
(dom f2) /\ ].x0,(x0 + r1).[ c= dom f2
by XBOOLE_1:17;
then
rng (seq ^\ k) c= dom f2
by A25, XBOOLE_1:1;
then A28:
rng (seq ^\ k) c= (dom f2) /\ (right_open_halfline x0)
by A20, XBOOLE_1:19;
then A29:
lim (f2 /* (seq ^\ k)) = lim_right (
f2,
x0)
by A2, A10, A26, Def8;
A30:
(dom f1) /\ ].x0,(x0 + r1).[ c= dom f1
by XBOOLE_1:17;
then
rng (seq ^\ k) c= dom f1
by A24, XBOOLE_1:1;
then A31:
rng (seq ^\ k) c= (dom f1) /\ (right_open_halfline x0)
by A20, XBOOLE_1:19;
then A32:
lim (f1 /* (seq ^\ k)) = lim_right (
f1,
x0)
by A1, A10, A26, Def8;
A33:
now for n being Nat holds
( (f1 /* (seq ^\ k)) . n <= (f /* (seq ^\ k)) . n & (f /* (seq ^\ k)) . n <= (f2 /* (seq ^\ k)) . n )let n be
Nat;
( (f1 /* (seq ^\ k)) . n <= (f /* (seq ^\ k)) . n & (f /* (seq ^\ k)) . n <= (f2 /* (seq ^\ k)) . n )A34:
n in NAT
by ORDINAL1:def 12;
A35:
(seq ^\ k) . n in rng (seq ^\ k)
by VALUED_0:28;
then
f . ((seq ^\ k) . n) <= f2 . ((seq ^\ k) . n)
by A6, A23;
then A36:
(f /* (seq ^\ k)) . n <= f2 . ((seq ^\ k) . n)
by A14, A22, FUNCT_2:108, XBOOLE_1:1, A34;
f1 . ((seq ^\ k) . n) <= f . ((seq ^\ k) . n)
by A6, A23, A35;
then
f1 . ((seq ^\ k) . n) <= (f /* (seq ^\ k)) . n
by A14, A22, FUNCT_2:108, A34, XBOOLE_1:1;
hence
(
(f1 /* (seq ^\ k)) . n <= (f /* (seq ^\ k)) . n &
(f /* (seq ^\ k)) . n <= (f2 /* (seq ^\ k)) . n )
by A30, A27, A24, A25, A36, FUNCT_2:108, XBOOLE_1:1, A34;
verum end; A37:
f2 /* (seq ^\ k) is
convergent
by A2, A10, A26, A28;
A38:
f1 /* (seq ^\ k) is
convergent
by A1, A10, A26, A31;
then
f /* (seq ^\ k) is
convergent
by A3, A32, A37, A29, A33, SEQ_2:19;
then A39:
(f /* seq) ^\ k is
convergent
by A12, A21, VALUED_0:27, XBOOLE_1:1;
hence
f /* seq is
convergent
by SEQ_4:21;
lim (f /* seq) = lim_right (f1,x0)
lim (f /* (seq ^\ k)) = lim_right (
f1,
x0)
by A3, A38, A32, A37, A29, A33, SEQ_2:20;
then
lim ((f /* seq) ^\ k) = lim_right (
f1,
x0)
by A12, A21, VALUED_0:27, XBOOLE_1:1;
hence
lim (f /* seq) = lim_right (
f1,
x0)
by A39, SEQ_4:22;
verum end; hence
f is_right_convergent_in x0
by A4;
( f is_right_convergent_in x0 & lim_right (f,x0) = lim_right (f1,x0) )hence
(
f is_right_convergent_in x0 &
lim_right (
f,
x0)
= lim_right (
f1,
x0) )
by A9, Def8;
verum end; suppose A40:
(
(dom f2) /\ ].x0,(x0 + r1).[ c= (dom f1) /\ ].x0,(x0 + r1).[ &
(dom f) /\ ].x0,(x0 + r1).[ c= (dom f2) /\ ].x0,(x0 + r1).[ )
;
( f is_right_convergent_in x0 & f is_right_convergent_in x0 & lim_right (f,x0) = lim_right (f1,x0) )A41:
now for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (right_open_halfline x0) holds
( f /* seq is convergent & lim (f /* seq) = lim_right (f1,x0) )let seq be
Real_Sequence;
( seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (right_open_halfline x0) implies ( f /* seq is convergent & lim (f /* seq) = lim_right (f1,x0) ) )assume that A42:
seq is
convergent
and A43:
lim seq = x0
and A44:
rng seq c= (dom f) /\ (right_open_halfline x0)
;
( f /* seq is convergent & lim (f /* seq) = lim_right (f1,x0) )
x0 < (lim seq) + r1
by A5, A43, Lm1;
then consider k being
Nat such that A45:
for
n being
Nat st
k <= n holds
seq . n < x0 + r1
by A42, A43, Th2;
A46:
rng (seq ^\ k) c= rng seq
by VALUED_0:21;
(dom f) /\ (right_open_halfline x0) c= right_open_halfline x0
by XBOOLE_1:17;
then
rng seq c= right_open_halfline x0
by A44, XBOOLE_1:1;
then A47:
rng (seq ^\ k) c= right_open_halfline x0
by A46, XBOOLE_1:1;
then A51:
rng (seq ^\ k) c= ].x0,(x0 + r1).[
by TARSKI:def 3;
].x0,(x0 + r1).[ c= right_open_halfline x0
by XXREAL_1:247;
then A52:
rng (seq ^\ k) c= right_open_halfline x0
by A51, XBOOLE_1:1;
A53:
(dom f) /\ (right_open_halfline x0) c= dom f
by XBOOLE_1:17;
then A54:
rng seq c= dom f
by A44, XBOOLE_1:1;
then
rng (seq ^\ k) c= dom f
by A46, XBOOLE_1:1;
then A55:
rng (seq ^\ k) c= (dom f) /\ ].x0,(x0 + r1).[
by A51, XBOOLE_1:19;
then A56:
rng (seq ^\ k) c= (dom f2) /\ ].x0,(x0 + r1).[
by A40, XBOOLE_1:1;
then A57:
rng (seq ^\ k) c= (dom f1) /\ ].x0,(x0 + r1).[
by A40, XBOOLE_1:1;
A58:
lim (seq ^\ k) = x0
by A42, A43, SEQ_4:20;
A59:
(dom f2) /\ ].x0,(x0 + r1).[ c= dom f2
by XBOOLE_1:17;
then
rng (seq ^\ k) c= dom f2
by A56, XBOOLE_1:1;
then A60:
rng (seq ^\ k) c= (dom f2) /\ (right_open_halfline x0)
by A52, XBOOLE_1:19;
then A61:
lim (f2 /* (seq ^\ k)) = lim_right (
f2,
x0)
by A2, A42, A58, Def8;
A62:
(dom f1) /\ ].x0,(x0 + r1).[ c= dom f1
by XBOOLE_1:17;
then
rng (seq ^\ k) c= dom f1
by A57, XBOOLE_1:1;
then A63:
rng (seq ^\ k) c= (dom f1) /\ (right_open_halfline x0)
by A52, XBOOLE_1:19;
then A64:
lim (f1 /* (seq ^\ k)) = lim_right (
f1,
x0)
by A1, A42, A58, Def8;
A65:
now for n being Nat holds
( (f1 /* (seq ^\ k)) . n <= (f /* (seq ^\ k)) . n & (f /* (seq ^\ k)) . n <= (f2 /* (seq ^\ k)) . n )let n be
Nat;
( (f1 /* (seq ^\ k)) . n <= (f /* (seq ^\ k)) . n & (f /* (seq ^\ k)) . n <= (f2 /* (seq ^\ k)) . n )A66:
n in NAT
by ORDINAL1:def 12;
A67:
(seq ^\ k) . n in rng (seq ^\ k)
by VALUED_0:28;
then
f . ((seq ^\ k) . n) <= f2 . ((seq ^\ k) . n)
by A6, A55;
then A68:
(f /* (seq ^\ k)) . n <= f2 . ((seq ^\ k) . n)
by A46, A54, FUNCT_2:108, XBOOLE_1:1, A66;
f1 . ((seq ^\ k) . n) <= f . ((seq ^\ k) . n)
by A6, A55, A67;
then
f1 . ((seq ^\ k) . n) <= (f /* (seq ^\ k)) . n
by A46, A54, FUNCT_2:108, A66, XBOOLE_1:1;
hence
(
(f1 /* (seq ^\ k)) . n <= (f /* (seq ^\ k)) . n &
(f /* (seq ^\ k)) . n <= (f2 /* (seq ^\ k)) . n )
by A62, A59, A56, A57, A68, FUNCT_2:108, XBOOLE_1:1, A66;
verum end; A69:
f2 /* (seq ^\ k) is
convergent
by A2, A42, A58, A60;
A70:
f1 /* (seq ^\ k) is
convergent
by A1, A42, A58, A63;
then
f /* (seq ^\ k) is
convergent
by A3, A64, A69, A61, A65, SEQ_2:19;
then A71:
(f /* seq) ^\ k is
convergent
by A44, A53, VALUED_0:27, XBOOLE_1:1;
hence
f /* seq is
convergent
by SEQ_4:21;
lim (f /* seq) = lim_right (f1,x0)
lim (f /* (seq ^\ k)) = lim_right (
f1,
x0)
by A3, A70, A64, A69, A61, A65, SEQ_2:20;
then
lim ((f /* seq) ^\ k) = lim_right (
f1,
x0)
by A44, A53, VALUED_0:27, XBOOLE_1:1;
hence
lim (f /* seq) = lim_right (
f1,
x0)
by A71, SEQ_4:22;
verum end; hence
f is_right_convergent_in x0
by A4;
( f is_right_convergent_in x0 & lim_right (f,x0) = lim_right (f1,x0) )hence
(
f is_right_convergent_in x0 &
lim_right (
f,
x0)
= lim_right (
f1,
x0) )
by A41, Def8;
verum end; end; end;
hence
( f is_right_convergent_in x0 & lim_right (f,x0) = lim_right (f1,x0) )
; verum