let x0 be Real; for f, f1, f2 being PartFunc of REAL,REAL st f1 is_left_convergent_in x0 & f2 is_left_convergent_in x0 & lim_left (f1,x0) = lim_left (f2,x0) & ( for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom f ) ) & ex r being Real st
( 0 < r & ( for g being Real st g in (dom f) /\ ].(x0 - r),x0.[ holds
( f1 . g <= f . g & f . g <= f2 . g ) ) & ( ( (dom f1) /\ ].(x0 - r),x0.[ c= (dom f2) /\ ].(x0 - r),x0.[ & (dom f) /\ ].(x0 - r),x0.[ c= (dom f1) /\ ].(x0 - r),x0.[ ) or ( (dom f2) /\ ].(x0 - r),x0.[ c= (dom f1) /\ ].(x0 - r),x0.[ & (dom f) /\ ].(x0 - r),x0.[ c= (dom f2) /\ ].(x0 - r),x0.[ ) ) ) holds
( f is_left_convergent_in x0 & lim_left (f,x0) = lim_left (f1,x0) )
let f, f1, f2 be PartFunc of REAL,REAL; ( f1 is_left_convergent_in x0 & f2 is_left_convergent_in x0 & lim_left (f1,x0) = lim_left (f2,x0) & ( for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom f ) ) & ex r being Real st
( 0 < r & ( for g being Real st g in (dom f) /\ ].(x0 - r),x0.[ holds
( f1 . g <= f . g & f . g <= f2 . g ) ) & ( ( (dom f1) /\ ].(x0 - r),x0.[ c= (dom f2) /\ ].(x0 - r),x0.[ & (dom f) /\ ].(x0 - r),x0.[ c= (dom f1) /\ ].(x0 - r),x0.[ ) or ( (dom f2) /\ ].(x0 - r),x0.[ c= (dom f1) /\ ].(x0 - r),x0.[ & (dom f) /\ ].(x0 - r),x0.[ c= (dom f2) /\ ].(x0 - r),x0.[ ) ) ) implies ( f is_left_convergent_in x0 & lim_left (f,x0) = lim_left (f1,x0) ) )
assume that
A1:
f1 is_left_convergent_in x0
and
A2:
f2 is_left_convergent_in x0
and
A3:
lim_left (f1,x0) = lim_left (f2,x0)
and
A4:
for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom f )
; ( for r being Real holds
( not 0 < r or ex g being Real st
( g in (dom f) /\ ].(x0 - r),x0.[ & not ( f1 . g <= f . g & f . g <= f2 . g ) ) or ( not ( (dom f1) /\ ].(x0 - r),x0.[ c= (dom f2) /\ ].(x0 - r),x0.[ & (dom f) /\ ].(x0 - r),x0.[ c= (dom f1) /\ ].(x0 - r),x0.[ ) & not ( (dom f2) /\ ].(x0 - r),x0.[ c= (dom f1) /\ ].(x0 - r),x0.[ & (dom f) /\ ].(x0 - r),x0.[ c= (dom f2) /\ ].(x0 - r),x0.[ ) ) ) or ( f is_left_convergent_in x0 & lim_left (f,x0) = lim_left (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.[ holds
( f1 . g <= f . g & f . g <= f2 . g )
and
A7:
( ( (dom f1) /\ ].(x0 - r1),x0.[ c= (dom f2) /\ ].(x0 - r1),x0.[ & (dom f) /\ ].(x0 - r1),x0.[ c= (dom f1) /\ ].(x0 - r1),x0.[ ) or ( (dom f2) /\ ].(x0 - r1),x0.[ c= (dom f1) /\ ].(x0 - r1),x0.[ & (dom f) /\ ].(x0 - r1),x0.[ c= (dom f2) /\ ].(x0 - r1),x0.[ ) )
; ( f is_left_convergent_in x0 & lim_left (f,x0) = lim_left (f1,x0) )
now ( f is_left_convergent_in x0 & f is_left_convergent_in x0 & lim_left (f,x0) = lim_left (f1,x0) )per cases
( ( (dom f1) /\ ].(x0 - r1),x0.[ c= (dom f2) /\ ].(x0 - r1),x0.[ & (dom f) /\ ].(x0 - r1),x0.[ c= (dom f1) /\ ].(x0 - r1),x0.[ ) or ( (dom f2) /\ ].(x0 - r1),x0.[ c= (dom f1) /\ ].(x0 - r1),x0.[ & (dom f) /\ ].(x0 - r1),x0.[ c= (dom f2) /\ ].(x0 - r1),x0.[ ) )
by A7;
suppose A8:
(
(dom f1) /\ ].(x0 - r1),x0.[ c= (dom f2) /\ ].(x0 - r1),x0.[ &
(dom f) /\ ].(x0 - r1),x0.[ c= (dom f1) /\ ].(x0 - r1),x0.[ )
;
( f is_left_convergent_in x0 & f is_left_convergent_in x0 & lim_left (f,x0) = lim_left (f1,x0) )A9:
now for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (left_open_halfline x0) holds
( f /* seq is convergent & lim (f /* seq) = lim_left (f1,x0) )let seq be
Real_Sequence;
( seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (left_open_halfline x0) implies ( f /* seq is convergent & lim (f /* seq) = lim_left (f1,x0) ) )assume that A10:
seq is
convergent
and A11:
lim seq = x0
and A12:
rng seq c= (dom f) /\ (left_open_halfline x0)
;
( f /* seq is convergent & lim (f /* seq) = lim_left (f1,x0) )
x0 - r1 < lim seq
by A5, A11, Lm1;
then consider k being
Nat such that A13:
for
n being
Nat st
k <= n holds
x0 - r1 < seq . n
by A10, Th1;
A14:
rng (seq ^\ k) c= rng seq
by VALUED_0:21;
(dom f) /\ (left_open_halfline x0) c= left_open_halfline x0
by XBOOLE_1:17;
then
rng seq c= left_open_halfline x0
by A12, XBOOLE_1:1;
then A15:
rng (seq ^\ k) c= left_open_halfline x0
by A14, XBOOLE_1:1;
then A19:
rng (seq ^\ k) c= ].(x0 - r1),x0.[
by TARSKI:def 3;
].(x0 - r1),x0.[ c= left_open_halfline x0
by XXREAL_1:263;
then A20:
rng (seq ^\ k) c= left_open_halfline x0
by A19, XBOOLE_1:1;
A21:
(dom f) /\ (left_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 - r1),x0.[
by A19, XBOOLE_1:19;
then A24:
rng (seq ^\ k) c= (dom f1) /\ ].(x0 - r1),x0.[
by A8, XBOOLE_1:1;
then A25:
rng (seq ^\ k) c= (dom f2) /\ ].(x0 - r1),x0.[
by A8, XBOOLE_1:1;
A26:
lim (seq ^\ k) = x0
by A10, A11, SEQ_4:20;
A27:
(dom f2) /\ ].(x0 - r1),x0.[ 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) /\ (left_open_halfline x0)
by A20, XBOOLE_1:19;
then A29:
lim (f2 /* (seq ^\ k)) = lim_left (
f2,
x0)
by A2, A10, A26, Def7;
A30:
(dom f1) /\ ].(x0 - r1),x0.[ 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) /\ (left_open_halfline x0)
by A20, XBOOLE_1:19;
then A32:
lim (f1 /* (seq ^\ k)) = lim_left (
f1,
x0)
by A1, A10, A26, Def7;
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_left (f1,x0)
lim (f /* (seq ^\ k)) = lim_left (
f1,
x0)
by A3, A38, A32, A37, A29, A33, SEQ_2:20;
then
lim ((f /* seq) ^\ k) = lim_left (
f1,
x0)
by A12, A21, VALUED_0:27, XBOOLE_1:1;
hence
lim (f /* seq) = lim_left (
f1,
x0)
by A39, SEQ_4:22;
verum end; hence
f is_left_convergent_in x0
by A4;
( f is_left_convergent_in x0 & lim_left (f,x0) = lim_left (f1,x0) )hence
(
f is_left_convergent_in x0 &
lim_left (
f,
x0)
= lim_left (
f1,
x0) )
by A9, Def7;
verum end; suppose A40:
(
(dom f2) /\ ].(x0 - r1),x0.[ c= (dom f1) /\ ].(x0 - r1),x0.[ &
(dom f) /\ ].(x0 - r1),x0.[ c= (dom f2) /\ ].(x0 - r1),x0.[ )
;
( f is_left_convergent_in x0 & f is_left_convergent_in x0 & lim_left (f,x0) = lim_left (f1,x0) )A41:
now for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (left_open_halfline x0) holds
( f /* seq is convergent & lim (f /* seq) = lim_left (f1,x0) )let seq be
Real_Sequence;
( seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (left_open_halfline x0) implies ( f /* seq is convergent & lim (f /* seq) = lim_left (f1,x0) ) )assume that A42:
seq is
convergent
and A43:
lim seq = x0
and A44:
rng seq c= (dom f) /\ (left_open_halfline x0)
;
( f /* seq is convergent & lim (f /* seq) = lim_left (f1,x0) )
x0 - r1 < lim seq
by A5, A43, Lm1;
then consider k being
Nat such that A45:
for
n being
Nat st
k <= n holds
x0 - r1 < seq . n
by A42, Th1;
A46:
rng (seq ^\ k) c= rng seq
by VALUED_0:21;
(dom f) /\ (left_open_halfline x0) c= left_open_halfline x0
by XBOOLE_1:17;
then
rng seq c= left_open_halfline x0
by A44, XBOOLE_1:1;
then A47:
rng (seq ^\ k) c= left_open_halfline x0
by A46, XBOOLE_1:1;
then A51:
rng (seq ^\ k) c= ].(x0 - r1),x0.[
by TARSKI:def 3;
].(x0 - r1),x0.[ c= left_open_halfline x0
by XXREAL_1:263;
then A52:
rng (seq ^\ k) c= left_open_halfline x0
by A51, XBOOLE_1:1;
A53:
(dom f) /\ (left_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 - r1),x0.[
by A51, XBOOLE_1:19;
then A56:
rng (seq ^\ k) c= (dom f2) /\ ].(x0 - r1),x0.[
by A40, XBOOLE_1:1;
then A57:
rng (seq ^\ k) c= (dom f1) /\ ].(x0 - r1),x0.[
by A40, XBOOLE_1:1;
A58:
lim (seq ^\ k) = x0
by A42, A43, SEQ_4:20;
A59:
(dom f2) /\ ].(x0 - r1),x0.[ 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) /\ (left_open_halfline x0)
by A52, XBOOLE_1:19;
then A61:
lim (f2 /* (seq ^\ k)) = lim_left (
f2,
x0)
by A2, A42, A58, Def7;
A62:
(dom f1) /\ ].(x0 - r1),x0.[ 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) /\ (left_open_halfline x0)
by A52, XBOOLE_1:19;
then A64:
lim (f1 /* (seq ^\ k)) = lim_left (
f1,
x0)
by A1, A42, A58, Def7;
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_left (f1,x0)
lim (f /* (seq ^\ k)) = lim_left (
f1,
x0)
by A3, A70, A64, A69, A61, A65, SEQ_2:20;
then
lim ((f /* seq) ^\ k) = lim_left (
f1,
x0)
by A44, A53, VALUED_0:27, XBOOLE_1:1;
hence
lim (f /* seq) = lim_left (
f1,
x0)
by A71, SEQ_4:22;
verum end; hence
f is_left_convergent_in x0
by A4;
( f is_left_convergent_in x0 & lim_left (f,x0) = lim_left (f1,x0) )hence
(
f is_left_convergent_in x0 &
lim_left (
f,
x0)
= lim_left (
f1,
x0) )
by A41, Def7;
verum end; end; end;
hence
( f is_left_convergent_in x0 & lim_left (f,x0) = lim_left (f1,x0) )
; verum