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) )
given r being Real such that A3: 0 < r and
A4: ( ( (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)

now :: thesis: lim_left (f1,x0) <= lim_left (f2,x0)

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 A4;

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

defpred S₁[ Nat, Real] means ( x0 - (1 / ($1 + 1)) < $2 & $2 < x0 & $2 in dom f1 );

A6: now :: thesis: for n being Element of NAT ex g being Element of REAL st S₁[n,g]

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

end;

consider s being Real_Sequence such that
A10: for n being Element of NAT holds S₁[n,s . n] from FUNCT_2:sch 3(A6);
A11: for n being Nat holds S₁[n,s . n]

proof

let n be Nat; :: thesis: S₁[n,s . n]
n in NAT by ORDINAL1:def 12;
hence S₁[n,s . n] by A10; :: thesis: verum

end;

A12: lim s = x0 by A11, Th5;
A13: rng s c= (dom f1) /\ (left_open_halfline x0) by A11, Th5;
A14: ].(x0 - r),x0.[ c= left_open_halfline x0 by XXREAL_1:263;
A15: s is convergent by A11, Th5;
x0 - r < x0 by A3, Lm1;
then consider k being Nat such that
A16: for n being Nat st k <= n holds
x0 - r < s . n by A15, A12, Th1;
A17: lim (s ^\ k) = x0 by A15, A12, SEQ_4:20;

now :: thesis: for x being object st x in rng (s ^\ k) holds
x in (dom f1) /\ ].(x0 - r),x0.[

let x be object ; :: 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
A18: (s ^\ k) . n = x by FUNCT_2:113;
s . (n + k) < x0 by A11;
then A19: (s ^\ k) . n < x0 by NAT_1:def 3;
s . (n + k) in dom f1 by A11;
then A20: (s ^\ k) . n in dom f1 by NAT_1:def 3;
x0 - r < s . (n + k) by A16, 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 A19;
then (s ^\ k) . n in ].(x0 - r),x0.[ by RCOMP_1:def 2;
hence x in (dom f1) /\ ].(x0 - r),x0.[ by A18, A20, XBOOLE_0:def 4; :: thesis: verum

end;

then A21: rng (s ^\ k) c= (dom f1) /\ ].(x0 - r),x0.[ by TARSKI:def 3;
then A22: rng (s ^\ k) c= (dom f2) /\ ].(x0 - r),x0.[ by A5, 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 A22, XBOOLE_1:1;
then A23: rng (s ^\ k) c= left_open_halfline x0 by A14, XBOOLE_1:1;
A24: (dom f2) /\ ].(x0 - r),x0.[ c= dom f2 by XBOOLE_1:17;
then rng (s ^\ k) c= dom f2 by A22, XBOOLE_1:1;
then A25: rng (s ^\ k) c= (dom f2) /\ (left_open_halfline x0) by A23, XBOOLE_1:19;
then A26: lim (f2 /* (s ^\ k)) = lim_left (f2,x0) by A2, A15, A17, Def7;
rng (s ^\ k) c= rng s by VALUED_0:21;
then A27: rng (s ^\ k) c= (dom f1) /\ (left_open_halfline x0) by A13, XBOOLE_1:1;
then A28: lim (f1 /* (s ^\ k)) = lim_left (f1,x0) by A1, A15, A17, Def7;
A29: (dom f1) /\ ].(x0 - r),x0.[ c= dom f1 by XBOOLE_1:17;

A30: now :: thesis: for n being Nat holds (f1 /* (s ^\ k)) . n <= (f2 /* (s ^\ k)) . n

let n be Nat; :: thesis: (f1 /* (s ^\ k)) . n <= (f2 /* (s ^\ k)) . n
A31: n in NAT by ORDINAL1:def 12;
(s ^\ k) . n in rng (s ^\ k) by VALUED_0:28;
then f1 . ((s ^\ k) . n) <= f2 . ((s ^\ k) . n) by A5, A21;
then f1 . ((s ^\ k) . n) <= (f2 /* (s ^\ k)) . n by A22, A24, FUNCT_2:108, XBOOLE_1:1, A31;
hence (f1 /* (s ^\ k)) . n <= (f2 /* (s ^\ k)) . n by A21, A29, FUNCT_2:108, XBOOLE_1:1, A31; :: thesis: verum

end;

A32: f2 /* (s ^\ k) is convergent by A2, A15, A17, A25;
f1 /* (s ^\ k) is convergent by A1, A15, A17, A27;
hence lim_left (f1,x0) <= lim_left (f2,x0) by A28, A32, A26, A30, SEQ_2:18; :: 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₁[ Nat, Real] means ( x0 - (1 / ($1 + 1)) < $2 & $2 < x0 & $2 in dom f2 );

A34: now :: thesis: for n being Element of NAT ex g being Element of REAL st S₁[n,g]

let n be Element of NAT ; :: thesis: ex g being Element of REAL st S₁[n,g]
0 < 1 / (n + 1) by XREAL_1:139;
then x0 - (1 / (n + 1)) < x0 - 0 by XREAL_1:15;
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;
reconsider g = g as Element of REAL by XREAL_0:def 1;
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: for n being Nat holds S₁[n,s . n]

proof

let n be Nat; :: thesis: S₁[n,s . n]
n in NAT by ORDINAL1:def 12;
hence S₁[n,s . n] by A38; :: thesis: verum

end;

A40: lim s = x0 by A39, Th5;
A41: rng s c= (dom f2) /\ (left_open_halfline x0) by A39, Th5;
A42: ].(x0 - r),x0.[ c= left_open_halfline x0 by XXREAL_1:263;
A43: s is convergent by A39, Th5;
x0 - r < x0 by A3, Lm1;
then consider k being Nat such that
A44: for n being Nat st k <= n holds
x0 - r < s . n by A43, A40, Th1;
A45: lim (s ^\ k) = x0 by A43, A40, SEQ_4:20;

A46: now :: thesis: for x being object st x in rng (s ^\ k) holds
x in (dom f2) /\ ].(x0 - r),x0.[

let x be object ; :: 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
A47: (s ^\ k) . n = x by FUNCT_2:113;
s . (n + k) < x0 by A39;
then A48: (s ^\ k) . n < x0 by NAT_1:def 3;
s . (n + k) in dom f2 by A39;
then A49: (s ^\ k) . n in dom f2 by NAT_1:def 3;
x0 - r < s . (n + k) by A44, 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 A48;
then (s ^\ k) . n in ].(x0 - r),x0.[ by RCOMP_1:def 2;
hence x in (dom f2) /\ ].(x0 - r),x0.[ by A47, A49, XBOOLE_0:def 4; :: thesis: verum

end;

then A50: rng (s ^\ k) c= (dom f2) /\ ].(x0 - r),x0.[ by TARSKI:def 3;
then A51: 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 A51, XBOOLE_1:1;
then A52: rng (s ^\ k) c= left_open_halfline x0 by A42, XBOOLE_1:1;
A53: (dom f1) /\ ].(x0 - r),x0.[ c= dom f1 by XBOOLE_1:17;
then rng (s ^\ k) c= dom f1 by A51, XBOOLE_1:1;
then A54: rng (s ^\ k) c= (dom f1) /\ (left_open_halfline x0) by A52, XBOOLE_1:19;
then A55: lim (f1 /* (s ^\ k)) = lim_left (f1,x0) by A1, A43, A45, Def7;
rng (s ^\ k) c= rng s by VALUED_0:21;
then A56: rng (s ^\ k) c= (dom f2) /\ (left_open_halfline x0) by A41, XBOOLE_1:1;
then A57: lim (f2 /* (s ^\ k)) = lim_left (f2,x0) by A2, A43, A45, Def7;
A58: (dom f2) /\ ].(x0 - r),x0.[ c= dom f2 by XBOOLE_1:17;

A59: now :: thesis: for n being Nat holds (f1 /* (s ^\ k)) . n <= (f2 /* (s ^\ k)) . n

let n be Nat; :: thesis: (f1 /* (s ^\ k)) . n <= (f2 /* (s ^\ k)) . n
A60: n in NAT by ORDINAL1:def 12;
(s ^\ k) . n in rng (s ^\ k) by VALUED_0:28;
then f1 . ((s ^\ k) . n) <= f2 . ((s ^\ k) . n) by A33, A46;
then f1 . ((s ^\ k) . n) <= (f2 /* (s ^\ k)) . n by A50, A58, FUNCT_2:108, XBOOLE_1:1, A60;
hence (f1 /* (s ^\ k)) . n <= (f2 /* (s ^\ k)) . n by A51, A53, FUNCT_2:108, XBOOLE_1:1, A60; :: thesis: verum

end;

A61: f1 /* (s ^\ k) is convergent by A1, A43, A45, A54;
f2 /* (s ^\ k) is convergent by A2, A43, A45, A56;
hence lim_left (f1,x0) <= lim_left (f2,x0) by A57, A61, A55, A59, SEQ_2:18; :: thesis: verum

end;

end;

end;

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