let x0 be Real; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: ( 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).[ ) ) ; :: thesis: ( f is_right_convergent_in x0 & lim_right (f,x0) = lim_right (f1,x0) )
now :: thesis: ( 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).[ ) ; :: thesis: ( f is_right_convergent_in x0 & f is_right_convergent_in x0 & lim_right (f,x0) = lim_right (f1,x0) )
A9: now :: thesis: 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; :: thesis: ( 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) ; :: thesis: ( 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;
now :: thesis: for x being object st x in rng (seq ^\ k) holds
x in ].x0,(x0 + r1).[
let x be object ; :: thesis: ( x in rng (seq ^\ k) implies x in ].x0,(x0 + r1).[ )
assume A16: x in rng (seq ^\ k) ; :: thesis: x in ].x0,(x0 + r1).[
then consider n being Element of NAT such that
A17: x = (seq ^\ k) . n by FUNCT_2:113;
(seq ^\ k) . n in right_open_halfline x0 by A15, A16, A17;
then (seq ^\ k) . n in { g where g is Real : x0 < g } by XXREAL_1:230;
then A18: ex g being Real st
( g = (seq ^\ k) . n & x0 < g ) ;
seq . (n + k) < x0 + r1 by A13, NAT_1:12;
then (seq ^\ k) . n < x0 + r1 by NAT_1:def 3;
then x in { g1 where g1 is Real : ( x0 < g1 & g1 < x0 + r1 ) } by A17, A18;
hence x in ].x0,(x0 + r1).[ by RCOMP_1:def 2; :: thesis: verum
end;
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 :: thesis: 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; :: thesis: ( (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; :: thesis: 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; :: thesis: 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; :: thesis: verum
end;
hence f is_right_convergent_in x0 by A4; :: thesis: ( 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; :: thesis: 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).[ ) ; :: thesis: ( f is_right_convergent_in x0 & f is_right_convergent_in x0 & lim_right (f,x0) = lim_right (f1,x0) )
A41: now :: thesis: 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; :: thesis: ( 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) ; :: thesis: ( 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;
now :: thesis: for x being object st x in rng (seq ^\ k) holds
x in ].x0,(x0 + r1).[
let x be object ; :: thesis: ( x in rng (seq ^\ k) implies x in ].x0,(x0 + r1).[ )
assume A48: x in rng (seq ^\ k) ; :: thesis: x in ].x0,(x0 + r1).[
then consider n being Element of NAT such that
A49: x = (seq ^\ k) . n by FUNCT_2:113;
(seq ^\ k) . n in right_open_halfline x0 by A47, A48, A49;
then (seq ^\ k) . n in { g where g is Real : x0 < g } by XXREAL_1:230;
then A50: ex g being Real st
( g = (seq ^\ k) . n & x0 < g ) ;
seq . (n + k) < x0 + r1 by A45, NAT_1:12;
then (seq ^\ k) . n < x0 + r1 by NAT_1:def 3;
then x in { g1 where g1 is Real : ( x0 < g1 & g1 < x0 + r1 ) } by A49, A50;
hence x in ].x0,(x0 + r1).[ by RCOMP_1:def 2; :: thesis: verum
end;
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 :: thesis: 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; :: thesis: ( (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; :: thesis: 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; :: thesis: 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; :: thesis: verum
end;
hence f is_right_convergent_in x0 by A4; :: thesis: ( 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; :: thesis: verum
end;
end;
end;
hence ( f is_right_convergent_in x0 & lim_right (f,x0) = lim_right (f1,x0) ) ; :: thesis: verum