let x0 be Real; :: thesis: for f1, f2 being PartFunc of REAL ,REAL st f1 is_right_convergent_in x0 & f2 is_right_convergent_in x0 & ex r being Real st
( 0 < r & ( ( (dom f1) /\ ].x0,(x0 + r).[ c= (dom f2) /\ ].x0,(x0 + r).[ & ( for g being Real st g in (dom f1) /\ ].x0,(x0 + r).[ holds
f1 . g <= f2 . g ) ) or ( (dom f2) /\ ].x0,(x0 + r).[ c= (dom f1) /\ ].x0,(x0 + r).[ & ( for g being Real st g in (dom f2) /\ ].x0,(x0 + r).[ holds
f1 . g <= f2 . g ) ) ) ) holds
lim_right f1,x0 <= lim_right f2,x0
let f1, f2 be PartFunc of REAL ,REAL ; :: thesis: ( f1 is_right_convergent_in x0 & f2 is_right_convergent_in x0 & ex r being Real st
( 0 < r & ( ( (dom f1) /\ ].x0,(x0 + r).[ c= (dom f2) /\ ].x0,(x0 + r).[ & ( for g being Real st g in (dom f1) /\ ].x0,(x0 + r).[ holds
f1 . g <= f2 . g ) ) or ( (dom f2) /\ ].x0,(x0 + r).[ c= (dom f1) /\ ].x0,(x0 + r).[ & ( for g being Real st g in (dom f2) /\ ].x0,(x0 + r).[ holds
f1 . g <= f2 . g ) ) ) ) implies lim_right f1,x0 <= lim_right f2,x0 )
assume that
A1: f1 is_right_convergent_in x0 and
A2: f2 is_right_convergent_in x0 ; :: thesis: ( for r being Real holds
( not 0 < r or ( not ( (dom f1) /\ ].x0,(x0 + r).[ c= (dom f2) /\ ].x0,(x0 + r).[ & ( for g being Real st g in (dom f1) /\ ].x0,(x0 + r).[ holds
f1 . g <= f2 . g ) ) & not ( (dom f2) /\ ].x0,(x0 + r).[ c= (dom f1) /\ ].x0,(x0 + r).[ & ( for g being Real st g in (dom f2) /\ ].x0,(x0 + r).[ holds
f1 . g <= f2 . g ) ) ) ) or lim_right f1,x0 <= lim_right f2,x0 )
A3: lim_right f2,x0 = lim_right f2,x0 ;
given r being Real such that A4: 0 < r and
A5: ( ( (dom f1) /\ ].x0,(x0 + r).[ c= (dom f2) /\ ].x0,(x0 + r).[ & ( for g being Real st g in (dom f1) /\ ].x0,(x0 + r).[ holds
f1 . g <= f2 . g ) ) or ( (dom f2) /\ ].x0,(x0 + r).[ c= (dom f1) /\ ].x0,(x0 + r).[ & ( for g being Real st g in (dom f2) /\ ].x0,(x0 + r).[ holds
f1 . g <= f2 . g ) ) ) ; :: thesis: lim_right f1,x0 <= lim_right f2,x0
A6: lim_right f1,x0 = lim_right f1,x0 ;
now
per cases ( ( (dom f1) /\ ].x0,(x0 + r).[ c= (dom f2) /\ ].x0,(x0 + r).[ & ( for g being Real st g in (dom f1) /\ ].x0,(x0 + r).[ holds
f1 . g <= f2 . g ) ) or ( (dom f2) /\ ].x0,(x0 + r).[ c= (dom f1) /\ ].x0,(x0 + r).[ & ( for g being Real st g in (dom f2) /\ ].x0,(x0 + r).[ holds
f1 . g <= f2 . g ) ) ) by A5;
suppose A7: ( (dom f1) /\ ].x0,(x0 + r).[ c= (dom f2) /\ ].x0,(x0 + r).[ & ( for g being Real st g in (dom f1) /\ ].x0,(x0 + r).[ holds
f1 . g <= f2 . g ) ) ; :: thesis: lim_right f1,x0 <= lim_right f2,x0
defpred S1[ Element of NAT , real number ] means ( x0 < $2 & $2 < x0 + (1 / ($1 + 1)) & $2 in dom f1 );
A8: now
let n be Element of NAT ; :: thesis: ex g being Real st S1[n,g]
x0 < x0 + (1 / (n + 1)) by Lm3;
then consider g being Real such that
A9: g < x0 + (1 / (n + 1)) and
A10: x0 < g and
A11: g in dom f1 by A1, Def4;
take g = g; :: thesis: S1[n,g]
thus S1[n,g] by A9, A10, A11; :: thesis: verum
end;
consider s being Real_Sequence such that
A12: for n being Element of NAT holds S1[n,s . n] from FUNCT_2:sch 3(A8);
A13: lim s = x0 by A12, Th6;
A14: rng s c= (dom f1) /\ (right_open_halfline x0) by A12, Th6;
A15: ].x0,(x0 + r).[ c= right_open_halfline x0 by XXREAL_1:247;
A16: s is convergent by A12, Th6;
x0 < x0 + r by A4, Lm1;
then consider k being Element of NAT such that
A17: for n being Element of NAT st k <= n holds
s . n < x0 + r by A16, A13, Th2;
A18: lim (s ^\ k) = x0 by A16, A13, SEQ_4:33;
now
let x be set ; :: thesis: ( x in rng (s ^\ k) implies x in (dom f1) /\ ].x0,(x0 + r).[ )
assume x in rng (s ^\ k) ; :: thesis: x in (dom f1) /\ ].x0,(x0 + r).[
then consider n being Element of NAT such that
A19: (s ^\ k) . n = x by FUNCT_2:190;
x0 < s . (n + k) by A12;
then A20: x0 < (s ^\ k) . n by NAT_1:def 3;
s . (n + k) in dom f1 by A12;
then A21: (s ^\ k) . n in dom f1 by NAT_1:def 3;
s . (n + k) < x0 + r by A17, NAT_1:12;
then (s ^\ k) . n < x0 + r by NAT_1:def 3;
then (s ^\ k) . n in { g2 where g2 is Real : ( x0 < g2 & g2 < x0 + r ) } by A20;
then (s ^\ k) . n in ].x0,(x0 + r).[ by RCOMP_1:def 2;
hence x in (dom f1) /\ ].x0,(x0 + r).[ by A19, A21, XBOOLE_0:def 4; :: thesis: verum
end;
then A22: rng (s ^\ k) c= (dom f1) /\ ].x0,(x0 + r).[ by TARSKI:def 3;
then A23: rng (s ^\ k) c= (dom f2) /\ ].x0,(x0 + r).[ by A7, XBOOLE_1:1;
(dom f2) /\ ].x0,(x0 + r).[ c= ].x0,(x0 + r).[ by XBOOLE_1:17;
then rng (s ^\ k) c= ].x0,(x0 + r).[ by A23, XBOOLE_1:1;
then A24: rng (s ^\ k) c= right_open_halfline x0 by A15, XBOOLE_1:1;
A25: (dom f2) /\ ].x0,(x0 + r).[ c= dom f2 by XBOOLE_1:17;
then rng (s ^\ k) c= dom f2 by A23, XBOOLE_1:1;
then A26: rng (s ^\ k) c= (dom f2) /\ (right_open_halfline x0) by A24, XBOOLE_1:19;
then A27: lim (f2 /* (s ^\ k)) = lim_right f2,x0 by A2, A16, A18, Def8;
rng (s ^\ k) c= rng s by VALUED_0:21;
then A28: rng (s ^\ k) c= (dom f1) /\ (right_open_halfline x0) by A14, XBOOLE_1:1;
then A29: lim (f1 /* (s ^\ k)) = lim_right f1,x0 by A1, A16, A18, Def8;
A30: (dom f1) /\ ].x0,(x0 + r).[ c= dom f1 by XBOOLE_1:17;
A31: now
let n be Element of NAT ; :: thesis: (f1 /* (s ^\ k)) . n <= (f2 /* (s ^\ k)) . n
(s ^\ k) . n in rng (s ^\ k) by VALUED_0:28;
then f1 . ((s ^\ k) . n) <= f2 . ((s ^\ k) . n) by A7, A22;
then f1 . ((s ^\ k) . n) <= (f2 /* (s ^\ k)) . n by A23, A25, FUNCT_2:185, XBOOLE_1:1;
hence (f1 /* (s ^\ k)) . n <= (f2 /* (s ^\ k)) . n by A22, A30, FUNCT_2:185, XBOOLE_1:1; :: thesis: verum
end;
A32: f2 /* (s ^\ k) is convergent by A2, A3, A16, A18, A26, Def8;
f1 /* (s ^\ k) is convergent by A1, A6, A16, A18, A28, Def8;
hence lim_right f1,x0 <= lim_right f2,x0 by A29, A32, A27, A31, SEQ_2:32; :: thesis: verum
end;
suppose A33: ( (dom f2) /\ ].x0,(x0 + r).[ c= (dom f1) /\ ].x0,(x0 + r).[ & ( for g being Real st g in (dom f2) /\ ].x0,(x0 + r).[ holds
f1 . g <= f2 . g ) ) ; :: thesis: lim_right f1,x0 <= lim_right f2,x0
defpred S1[ Element of NAT , real number ] means ( x0 < $2 & $2 < x0 + (1 / ($1 + 1)) & $2 in dom f2 );
A34: now
let n be Element of NAT ; :: thesis: ex g being Real st S1[n,g]
0 < 1 / (n + 1) by XREAL_1:141;
then x0 + 0 < x0 + (1 / (n + 1)) by XREAL_1:10;
then consider g being Real such that
A35: g < x0 + (1 / (n + 1)) and
A36: x0 < g and
A37: g in dom f2 by A2, Def4;
take g = g; :: thesis: S1[n,g]
thus S1[n,g] by A35, A36, A37; :: thesis: verum
end;
consider s being Real_Sequence such that
A38: for n being Element of NAT holds S1[n,s . n] from FUNCT_2:sch 3(A34);
A39: lim s = x0 by A38, Th6;
A40: rng s c= (dom f2) /\ (right_open_halfline x0) by A38, Th6;
A41: ].x0,(x0 + r).[ c= right_open_halfline x0 by XXREAL_1:247;
A42: s is convergent by A38, Th6;
x0 < x0 + r by A4, Lm1;
then consider k being Element of NAT such that
A43: for n being Element of NAT st k <= n holds
s . n < x0 + r by A42, A39, Th2;
A44: lim (s ^\ k) = x0 by A42, A39, SEQ_4:33;
A45: now
let x be set ; :: thesis: ( x in rng (s ^\ k) implies x in (dom f2) /\ ].x0,(x0 + r).[ )
assume x in rng (s ^\ k) ; :: thesis: x in (dom f2) /\ ].x0,(x0 + r).[
then consider n being Element of NAT such that
A46: (s ^\ k) . n = x by FUNCT_2:190;
x0 < s . (n + k) by A38;
then A47: x0 < (s ^\ k) . n by NAT_1:def 3;
s . (n + k) in dom f2 by A38;
then A48: (s ^\ k) . n in dom f2 by NAT_1:def 3;
s . (n + k) < x0 + r by A43, NAT_1:12;
then (s ^\ k) . n < x0 + r by NAT_1:def 3;
then (s ^\ k) . n in { g2 where g2 is Real : ( x0 < g2 & g2 < x0 + r ) } by A47;
then (s ^\ k) . n in ].x0,(x0 + r).[ by RCOMP_1:def 2;
hence x in (dom f2) /\ ].x0,(x0 + r).[ by A46, A48, XBOOLE_0:def 4; :: thesis: verum
end;
then A49: rng (s ^\ k) c= (dom f2) /\ ].x0,(x0 + r).[ by TARSKI:def 3;
then A50: rng (s ^\ k) c= (dom f1) /\ ].x0,(x0 + r).[ by A33, XBOOLE_1:1;
(dom f1) /\ ].x0,(x0 + r).[ c= ].x0,(x0 + r).[ by XBOOLE_1:17;
then rng (s ^\ k) c= ].x0,(x0 + r).[ by A50, XBOOLE_1:1;
then A51: rng (s ^\ k) c= right_open_halfline x0 by A41, XBOOLE_1:1;
A52: (dom f1) /\ ].x0,(x0 + r).[ c= dom f1 by XBOOLE_1:17;
then rng (s ^\ k) c= dom f1 by A50, XBOOLE_1:1;
then A53: rng (s ^\ k) c= (dom f1) /\ (right_open_halfline x0) by A51, XBOOLE_1:19;
then A54: lim (f1 /* (s ^\ k)) = lim_right f1,x0 by A1, A42, A44, Def8;
rng (s ^\ k) c= rng s by VALUED_0:21;
then A55: rng (s ^\ k) c= (dom f2) /\ (right_open_halfline x0) by A40, XBOOLE_1:1;
then A56: lim (f2 /* (s ^\ k)) = lim_right f2,x0 by A2, A42, A44, Def8;
A57: (dom f2) /\ ].x0,(x0 + r).[ c= dom f2 by XBOOLE_1:17;
A58: now
let n be Element of NAT ; :: thesis: (f1 /* (s ^\ k)) . n <= (f2 /* (s ^\ k)) . n
(s ^\ k) . n in rng (s ^\ k) by VALUED_0:28;
then f1 . ((s ^\ k) . n) <= f2 . ((s ^\ k) . n) by A33, A45;
then f1 . ((s ^\ k) . n) <= (f2 /* (s ^\ k)) . n by A49, A57, FUNCT_2:185, XBOOLE_1:1;
hence (f1 /* (s ^\ k)) . n <= (f2 /* (s ^\ k)) . n by A50, A52, FUNCT_2:185, XBOOLE_1:1; :: thesis: verum
end;
A59: f1 /* (s ^\ k) is convergent by A1, A6, A42, A44, A53, Def8;
f2 /* (s ^\ k) is convergent by A2, A3, A42, A44, A55, Def8;
hence lim_right f1,x0 <= lim_right f2,x0 by A56, A59, A54, A58, SEQ_2:32; :: thesis: verum
end;
end;
end;
hence lim_right f1,x0 <= lim_right f2,x0 ; :: thesis: verum