let x0 be Real; :: thesis: for f1, f2 being PartFunc of REAL,REAL st f1 is_left_convergent_in x0 & f2 is_left_convergent_in x0 & ex r being Real st
( 0 < r & ( ( (dom f1) /\ ].(x0 - r),x0.[ c= (dom f2) /\ ].(x0 - r),x0.[ & ( for g being Real st g in (dom f1) /\ ].(x0 - r),x0.[ holds
f1 . g <= f2 . g ) ) or ( (dom f2) /\ ].(x0 - r),x0.[ c= (dom f1) /\ ].(x0 - r),x0.[ & ( for g being Real st g in (dom f2) /\ ].(x0 - r),x0.[ holds
f1 . g <= f2 . g ) ) ) ) holds
lim_left (f1,x0) <= lim_left (f2,x0)
let f1, f2 be PartFunc of REAL,REAL; :: thesis: ( f1 is_left_convergent_in x0 & f2 is_left_convergent_in x0 & ex r being Real st
( 0 < r & ( ( (dom f1) /\ ].(x0 - r),x0.[ c= (dom f2) /\ ].(x0 - r),x0.[ & ( for g being Real st g in (dom f1) /\ ].(x0 - r),x0.[ holds
f1 . g <= f2 . g ) ) or ( (dom f2) /\ ].(x0 - r),x0.[ c= (dom f1) /\ ].(x0 - r),x0.[ & ( for g being Real st g in (dom f2) /\ ].(x0 - r),x0.[ holds
f1 . g <= f2 . g ) ) ) ) implies lim_left (f1,x0) <= lim_left (f2,x0) )
assume that
A1: f1 is_left_convergent_in x0 and
A2: f2 is_left_convergent_in x0 ; :: thesis: ( for r being Real holds
( not 0 < r or ( not ( (dom f1) /\ ].(x0 - r),x0.[ c= (dom f2) /\ ].(x0 - r),x0.[ & ( for g being Real st g in (dom f1) /\ ].(x0 - r),x0.[ holds
f1 . g <= f2 . g ) ) & not ( (dom f2) /\ ].(x0 - r),x0.[ c= (dom f1) /\ ].(x0 - r),x0.[ & ( for g being Real st g in (dom f2) /\ ].(x0 - r),x0.[ holds
f1 . g <= f2 . g ) ) ) ) or lim_left (f1,x0) <= lim_left (f2,x0) )
A3: lim_left (f2,x0) = lim_left (f2,x0) ;
given r being Real such that A4: 0 < r and
A5: ( ( (dom f1) /\ ].(x0 - r),x0.[ c= (dom f2) /\ ].(x0 - r),x0.[ & ( for g being Real st g in (dom f1) /\ ].(x0 - r),x0.[ holds
f1 . g <= f2 . g ) ) or ( (dom f2) /\ ].(x0 - r),x0.[ c= (dom f1) /\ ].(x0 - r),x0.[ & ( for g being Real st g in (dom f2) /\ ].(x0 - r),x0.[ holds
f1 . g <= f2 . g ) ) ) ; :: thesis: lim_left (f1,x0) <= lim_left (f2,x0)
A6: lim_left (f1,x0) = lim_left (f1,x0) ;

now

per cases ( ( (dom f1) /\ ].(x0 - r),x0.[ c= (dom f2) /\ ].(x0 - r),x0.[ & ( for g being Real st g in (dom f1) /\ ].(x0 - r),x0.[ holds
f1 . g <= f2 . g ) ) or ( (dom f2) /\ ].(x0 - r),x0.[ c= (dom f1) /\ ].(x0 - r),x0.[ & ( for g being Real st g in (dom f2) /\ ].(x0 - r),x0.[ holds
f1 . g <= f2 . g ) ) ) by A5;

suppose A7: ( (dom f1) /\ ].(x0 - r),x0.[ c= (dom f2) /\ ].(x0 - r),x0.[ & ( for g being Real st g in (dom f1) /\ ].(x0 - r),x0.[ holds
f1 . g <= f2 . g ) ) ; :: thesis: lim_left (f1,x0) <= lim_left (f2,x0)

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

A8: now

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

end;

consider s being Real_Sequence such that
A12: for n being Element of NAT holds S₁[n,s . n] from FUNCT_2:sch 3(A8);
A13: lim s = x0 by A12, Th5;
A14: rng s c= (dom f1) /\ (left_open_halfline x0) by A12, Th5;
A15: ].(x0 - r),x0.[ c= left_open_halfline x0 by XXREAL_1:263;
A16: s is convergent by A12, Th5;
x0 - r < x0 by A4, Lm1;
then consider k being Element of NAT such that
A17: for n being Element of NAT st k <= n holds
x0 - r < s . n by A16, A13, Th1;
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 - r),x0.[ )
assume x in rng (s ^\ k) ; :: thesis: x in (dom f1) /\ ].(x0 - r),x0.[
then consider n being Element of NAT such that
A19: (s ^\ k) . n = x by FUNCT_2:190;
s . (n + k) < x0 by A12;
then A20: (s ^\ k) . n < x0 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;
x0 - r < s . (n + k) by A17, NAT_1:12;
then x0 - r < (s ^\ k) . n by NAT_1:def 3;
then (s ^\ k) . n in { g2 where g2 is Real : ( x0 - r < g2 & g2 < x0 ) } by A20;
then (s ^\ k) . n in ].(x0 - r),x0.[ by RCOMP_1:def 2;
hence x in (dom f1) /\ ].(x0 - r),x0.[ by A19, A21, XBOOLE_0:def 4; :: thesis: verum

end;

then A22: rng (s ^\ k) c= (dom f1) /\ ].(x0 - r),x0.[ by TARSKI:def 3;
then A23: rng (s ^\ k) c= (dom f2) /\ ].(x0 - r),x0.[ by A7, XBOOLE_1:1;
(dom f2) /\ ].(x0 - r),x0.[ c= ].(x0 - r),x0.[ by XBOOLE_1:17;
then rng (s ^\ k) c= ].(x0 - r),x0.[ by A23, XBOOLE_1:1;
then A24: rng (s ^\ k) c= left_open_halfline x0 by A15, XBOOLE_1:1;
A25: (dom f2) /\ ].(x0 - r),x0.[ 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) /\ (left_open_halfline x0) by A24, XBOOLE_1:19;
then A27: lim (f2 /* (s ^\ k)) = lim_left (f2,x0) by A2, A16, A18, Def7;
rng (s ^\ k) c= rng s by VALUED_0:21;
then A28: rng (s ^\ k) c= (dom f1) /\ (left_open_halfline x0) by A14, XBOOLE_1:1;
then A29: lim (f1 /* (s ^\ k)) = lim_left (f1,x0) by A1, A16, A18, Def7;
A30: (dom f1) /\ ].(x0 - r),x0.[ 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, Def7;
f1 /* (s ^\ k) is convergent by A1, A6, A16, A18, A28, Def7;
hence lim_left (f1,x0) <= lim_left (f2,x0) by A29, A32, A27, A31, SEQ_2:32; :: thesis: verum

end;

suppose A33: ( (dom f2) /\ ].(x0 - r),x0.[ c= (dom f1) /\ ].(x0 - r),x0.[ & ( for g being Real st g in (dom f2) /\ ].(x0 - r),x0.[ holds
f1 . g <= f2 . g ) ) ; :: thesis: lim_left (f1,x0) <= lim_left (f2,x0)

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

A34: 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 - (1 / (n + 1)) < x0 - 0 by XREAL_1:17;
then consider g being Real such that
A35: x0 - (1 / (n + 1)) < g and
A36: g < x0 and
A37: g in dom f2 by A2, Def1;
take g = g; :: thesis: S₁[n,g]
thus S₁[n,g] by A35, A36, A37; :: thesis: verum

end;

consider s being Real_Sequence such that
A38: for n being Element of NAT holds S₁[n,s . n] from FUNCT_2:sch 3(A34);
A39: lim s = x0 by A38, Th5;
A40: rng s c= (dom f2) /\ (left_open_halfline x0) by A38, Th5;
A41: ].(x0 - r),x0.[ c= left_open_halfline x0 by XXREAL_1:263;
A42: s is convergent by A38, Th5;
x0 - r < x0 by A4, Lm1;
then consider k being Element of NAT such that
A43: for n being Element of NAT st k <= n holds
x0 - r < s . n by A42, A39, Th1;
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 - r),x0.[ )
assume x in rng (s ^\ k) ; :: thesis: x in (dom f2) /\ ].(x0 - r),x0.[
then consider n being Element of NAT such that
A46: (s ^\ k) . n = x by FUNCT_2:190;
s . (n + k) < x0 by A38;
then A47: (s ^\ k) . n < x0 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;
x0 - r < s . (n + k) by A43, NAT_1:12;
then x0 - r < (s ^\ k) . n by NAT_1:def 3;
then (s ^\ k) . n in { g2 where g2 is Real : ( x0 - r < g2 & g2 < x0 ) } by A47;
then (s ^\ k) . n in ].(x0 - r),x0.[ by RCOMP_1:def 2;
hence x in (dom f2) /\ ].(x0 - r),x0.[ by A46, A48, XBOOLE_0:def 4; :: thesis: verum

end;

then A49: rng (s ^\ k) c= (dom f2) /\ ].(x0 - r),x0.[ by TARSKI:def 3;
then A50: rng (s ^\ k) c= (dom f1) /\ ].(x0 - r),x0.[ by A33, XBOOLE_1:1;
(dom f1) /\ ].(x0 - r),x0.[ c= ].(x0 - r),x0.[ by XBOOLE_1:17;
then rng (s ^\ k) c= ].(x0 - r),x0.[ by A50, XBOOLE_1:1;
then A51: rng (s ^\ k) c= left_open_halfline x0 by A41, XBOOLE_1:1;
A52: (dom f1) /\ ].(x0 - r),x0.[ 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) /\ (left_open_halfline x0) by A51, XBOOLE_1:19;
then A54: lim (f1 /* (s ^\ k)) = lim_left (f1,x0) by A1, A42, A44, Def7;
rng (s ^\ k) c= rng s by VALUED_0:21;
then A55: rng (s ^\ k) c= (dom f2) /\ (left_open_halfline x0) by A40, XBOOLE_1:1;
then A56: lim (f2 /* (s ^\ k)) = lim_left (f2,x0) by A2, A42, A44, Def7;
A57: (dom f2) /\ ].(x0 - r),x0.[ 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, Def7;
f2 /* (s ^\ k) is convergent by A2, A3, A42, A44, A55, Def7;
hence lim_left (f1,x0) <= lim_left (f2,x0) by A56, A59, A54, A58, SEQ_2:32; :: thesis: verum

end;

end;

end;

hence lim_left (f1,x0) <= lim_left (f2,x0) ; :: thesis: verum