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 A1: ( f1 is_right_convergent_in x0 & 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 )
given r being Real such that A2: 0 < r and
A3: ( ( (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
A4: ( lim_right f1,x0 = lim_right f1,x0 & lim_right f2,x0 = lim_right f2,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 A3;

suppose 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 ) ) ; :: thesis: lim_right f1,x0 <= lim_right f2,x0

defpred S₁[ Element of NAT , real number ] means ( x0 < $2 & $2 < x0 + (1 / ($1 + 1)) & $2 in dom f1 );

A6: now

let n be Element of NAT ; :: thesis: ex g being Real st S₁[n,g]
x0 < x0 + (1 / (n + 1)) by Lm3;
then consider g being Real such that
A7: ( g < x0 + (1 / (n + 1)) & x0 < g & g in dom f1 ) by A1, Def4;
take g = g; :: thesis: S₁[n,g]
thus S₁[n,g] by A7; :: thesis: verum

end;

consider s being Real_Sequence such that
A8: for n being Element of NAT holds S₁[n,s . n] from FUNCT_2:sch 3(A6);
A9: ( s is convergent & lim s = x0 & rng s c= (dom f1) /\ (right_open_halfline x0) ) by A8, Th6;
x0 < x0 + r by A2, Lm1;
then consider k being Element of NAT such that
A10: for n being Element of NAT st k <= n holds
s . n < x0 + r by A9, Th2;
A11: ( s ^\ k is convergent & lim (s ^\ k) = x0 ) by A9, SEQ_4:33;
rng (s ^\ k) c= rng s by VALUED_0:21;
then rng (s ^\ k) c= (dom f1) /\ (right_open_halfline x0) by A9, XBOOLE_1:1;
then A12: ( f1 /* (s ^\ k) is convergent & lim (f1 /* (s ^\ k)) = lim_right f1,x0 ) by A1, A4, A11, Def8;

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
A13: (s ^\ k) . n = x by FUNCT_2:190;
s . (n + k) < x0 + r by A10, NAT_1:12;
then A14: (s ^\ k) . n < x0 + r by NAT_1:def 3;
( x0 < s . (n + k) & s . (n + k) in dom f1 ) by A8;
then A15: ( x0 < (s ^\ k) . n & (s ^\ k) . n in dom f1 ) by NAT_1:def 3;
then (s ^\ k) . n in { g2 where g2 is Real : ( x0 < g2 & g2 < x0 + r ) } by A14;
then (s ^\ k) . n in ].x0,(x0 + r).[ by RCOMP_1:def 2;
hence x in (dom f1) /\ ].x0,(x0 + r).[ by A13, A15, XBOOLE_0:def 4; :: thesis: verum

end;

then A16: rng (s ^\ k) c= (dom f1) /\ ].x0,(x0 + r).[ by TARSKI:def 3;
then A17: rng (s ^\ k) c= (dom f2) /\ ].x0,(x0 + r).[ by A5, XBOOLE_1:1;
A18: ( (dom f2) /\ ].x0,(x0 + r).[ c= dom f2 & (dom f2) /\ ].x0,(x0 + r).[ c= ].x0,(x0 + r).[ ) by XBOOLE_1:17;
then A19: ( rng (s ^\ k) c= dom f2 & rng (s ^\ k) c= ].x0,(x0 + r).[ ) by A17, XBOOLE_1:1;
].x0,(x0 + r).[ c= right_open_halfline x0 by XXREAL_1:247;
then rng (s ^\ k) c= right_open_halfline x0 by A19, XBOOLE_1:1;
then rng (s ^\ k) c= (dom f2) /\ (right_open_halfline x0) by A19, XBOOLE_1:19;
then A20: ( f2 /* (s ^\ k) is convergent & lim (f2 /* (s ^\ k)) = lim_right f2,x0 ) by A1, A4, A11, Def8;
A21: (dom f1) /\ ].x0,(x0 + r).[ c= dom f1 by XBOOLE_1:17;

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 A5, A16;
then f1 . ((s ^\ k) . n) <= (f2 /* (s ^\ k)) . n by A17, A18, FUNCT_2:185, XBOOLE_1:1;
hence (f1 /* (s ^\ k)) . n <= (f2 /* (s ^\ k)) . n by A16, A21, FUNCT_2:185, XBOOLE_1:1; :: thesis: verum

end;

hence lim_right f1,x0 <= lim_right f2,x0 by A12, A20, SEQ_2:32; :: thesis: verum

end;

suppose A22: ( (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 S₁[ Element of NAT , real number ] means ( x0 < $2 & $2 < x0 + (1 / ($1 + 1)) & $2 in dom f2 );

A23: now

let n be Element of NAT ; :: thesis: ex g being Real st S₁[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
A24: ( g < x0 + (1 / (n + 1)) & x0 < g & g in dom f2 ) by A1, Def4;
take g = g; :: thesis: S₁[n,g]
thus S₁[n,g] by A24; :: thesis: verum

end;

consider s being Real_Sequence such that
A25: for n being Element of NAT holds S₁[n,s . n] from FUNCT_2:sch 3(A23);
A26: ( s is convergent & lim s = x0 & rng s c= (dom f2) /\ (right_open_halfline x0) ) by A25, Th6;
x0 < x0 + r by A2, Lm1;
then consider k being Element of NAT such that
A27: for n being Element of NAT st k <= n holds
s . n < x0 + r by A26, Th2;
A28: ( s ^\ k is convergent & lim (s ^\ k) = x0 ) by A26, SEQ_4:33;
rng (s ^\ k) c= rng s by VALUED_0:21;
then rng (s ^\ k) c= (dom f2) /\ (right_open_halfline x0) by A26, XBOOLE_1:1;
then A29: ( f2 /* (s ^\ k) is convergent & lim (f2 /* (s ^\ k)) = lim_right f2,x0 ) by A1, A4, A28, Def8;

A30: 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
A31: (s ^\ k) . n = x by FUNCT_2:190;
s . (n + k) < x0 + r by A27, NAT_1:12;
then A32: (s ^\ k) . n < x0 + r by NAT_1:def 3;
( x0 < s . (n + k) & s . (n + k) in dom f2 ) by A25;
then A33: ( x0 < (s ^\ k) . n & (s ^\ k) . n in dom f2 ) by NAT_1:def 3;
then (s ^\ k) . n in { g2 where g2 is Real : ( x0 < g2 & g2 < x0 + r ) } by A32;
then (s ^\ k) . n in ].x0,(x0 + r).[ by RCOMP_1:def 2;
hence x in (dom f2) /\ ].x0,(x0 + r).[ by A31, A33, XBOOLE_0:def 4; :: thesis: verum

end;

then A34: rng (s ^\ k) c= (dom f2) /\ ].x0,(x0 + r).[ by TARSKI:def 3;
then A35: rng (s ^\ k) c= (dom f1) /\ ].x0,(x0 + r).[ by A22, XBOOLE_1:1;
A36: ( (dom f1) /\ ].x0,(x0 + r).[ c= dom f1 & (dom f1) /\ ].x0,(x0 + r).[ c= ].x0,(x0 + r).[ ) by XBOOLE_1:17;
then A37: ( rng (s ^\ k) c= dom f1 & rng (s ^\ k) c= ].x0,(x0 + r).[ ) by A35, XBOOLE_1:1;
].x0,(x0 + r).[ c= right_open_halfline x0 by XXREAL_1:247;
then rng (s ^\ k) c= right_open_halfline x0 by A37, XBOOLE_1:1;
then rng (s ^\ k) c= (dom f1) /\ (right_open_halfline x0) by A37, XBOOLE_1:19;
then A38: ( f1 /* (s ^\ k) is convergent & lim (f1 /* (s ^\ k)) = lim_right f1,x0 ) by A1, A4, A28, Def8;
A39: (dom f2) /\ ].x0,(x0 + r).[ c= dom f2 by XBOOLE_1:17;

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 A22, A30;
then f1 . ((s ^\ k) . n) <= (f2 /* (s ^\ k)) . n by A34, A39, FUNCT_2:185, XBOOLE_1:1;
hence (f1 /* (s ^\ k)) . n <= (f2 /* (s ^\ k)) . n by A35, A36, FUNCT_2:185, XBOOLE_1:1; :: thesis: verum

end;

hence lim_right f1,x0 <= lim_right f2,x0 by A29, A38, SEQ_2:32; :: thesis: verum

end;

end;

end;

hence lim_right f1,x0 <= lim_right f2,x0 ; :: thesis: verum