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

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

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

suppose A5: ( (dom f1) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) c= (dom f2) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) & ( for g being Real st g in (dom f1) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) holds
f1 . g <= f2 . g ) ) ; :: thesis: lim (f1,x0) <= lim (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 g1 being Element of REAL st S₁[n,g1]

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

end;

consider s being Real_Sequence such that
A11: for n being Element of NAT holds S₁[n,s . n] from FUNCT_2:sch 3(A6);
A12: lim s = x0 by A11, Th6;
A13: rng s c= (dom f1) \ {x0} by A11, Th6;
A14: s is convergent by A11, Th6;
x0 - r < x0 by A3, Lm1;
then consider k being Nat such that
A15: for n being Nat st k <= n holds
x0 - r < s . n by A14, A12, LIMFUNC2:1;
A16: lim (s ^\ k) = x0 by A14, A12, SEQ_4:20;
rng (s ^\ k) c= rng s by VALUED_0:21;
then A17: rng (s ^\ k) c= (dom f1) \ {x0} by A13;
then A18: lim (f1 /* (s ^\ k)) = lim (f1,x0) by A1, A14, A16, Def4;

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

let x be object ; :: thesis: ( x in rng (s ^\ k) implies x in (dom f1) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) )
assume x in rng (s ^\ k) ; :: thesis: x in (dom f1) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[)
then consider n being Element of NAT such that
A19: (s ^\ k) . n = x by FUNCT_2:113;
A20: n + k in NAT by ORDINAL1:def 12;
s . (n + k) < x0 by A11, A20;
then A21: (s ^\ k) . n < x0 by NAT_1:def 3;
x0 - r < s . (n + k) by A15, 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 A21;
then (s ^\ k) . n in ].(x0 - r),x0.[ by RCOMP_1:def 2;
then A22: (s ^\ k) . n in ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ by XBOOLE_0:def 3;
s . (n + k) in dom f1 by A11, A20;
then (s ^\ k) . n in dom f1 by NAT_1:def 3;
hence x in (dom f1) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) by A19, A22, XBOOLE_0:def 4; :: thesis: verum

end;

then A23: rng (s ^\ k) c= (dom f1) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) ;
then A24: rng (s ^\ k) c= (dom f2) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) by A5;

A25: 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
A26: 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, A23;
then f1 . ((s ^\ k) . n) <= (f2 /* (s ^\ k)) . n by A24, FUNCT_2:108, XBOOLE_1:18, A26;
hence (f1 /* (s ^\ k)) . n <= (f2 /* (s ^\ k)) . n by A23, FUNCT_2:108, XBOOLE_1:18, A26; :: thesis: verum

end;

A27: rng (s ^\ k) c= dom f2 by A24, XBOOLE_1:18;
A28: rng (s ^\ k) c= (dom f2) \ {x0}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (s ^\ k) or x in (dom f2) \ {x0} )
assume A29: x in rng (s ^\ k) ; :: thesis: x in (dom f2) \ {x0}
then not x in {x0} by A17, XBOOLE_0:def 5;
hence x in (dom f2) \ {x0} by A27, A29, XBOOLE_0:def 5; :: thesis: verum

end;

then A30: lim (f2 /* (s ^\ k)) = lim (f2,x0) by A2, A14, A16, Def4;
A31: f2 /* (s ^\ k) is convergent by A2, A14, A16, A28;
f1 /* (s ^\ k) is convergent by A1, A14, A16, A17;
hence lim (f1,x0) <= lim (f2,x0) by A18, A31, A30, A25, SEQ_2:18; :: thesis: verum

end;

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

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

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

let n be Element of NAT ; :: thesis: ex g1 being Element of REAL st S₁[n,g1]
A34: x0 < x0 + 1 by Lm1;
x0 - (1 / (n + 1)) < x0 by Lm3;
then consider g1, g2 being Real such that
A35: x0 - (1 / (n + 1)) < g1 and
A36: g1 < x0 and
A37: g1 in dom f2 and
g2 < x0 + 1 and
x0 < g2 and
g2 in dom f2 by A2, A34;
reconsider g1 = g1 as Element of REAL by XREAL_0:def 1;
take g1 = g1; :: thesis: S₁[n,g1]
thus S₁[n,g1] 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(A33);
A39: lim s = x0 by A38, Th6;
A40: rng s c= (dom f2) \ {x0} by A38, Th6;
A41: s is convergent by A38, Th6;
x0 - r < x0 by A3, Lm1;
then consider k being Nat such that
A42: for n being Nat st k <= n holds
x0 - r < s . n by A41, A39, LIMFUNC2:1;
A43: lim (s ^\ k) = x0 by A41, A39, SEQ_4:20;
rng (s ^\ k) c= rng s by VALUED_0:21;
then A44: rng (s ^\ k) c= (dom f2) \ {x0} by A40;
then A45: lim (f2 /* (s ^\ k)) = lim (f2,x0) by A2, A41, A43, Def4;

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

let x be object ; :: thesis: ( x in rng (s ^\ k) implies x in (dom f2) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) )
assume x in rng (s ^\ k) ; :: thesis: x in (dom f2) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[)
then consider n being Element of NAT such that
A47: (s ^\ k) . n = x by FUNCT_2:113;
A48: n + k in NAT by ORDINAL1:def 12;
s . (n + k) < x0 by A38, A48;
then A49: (s ^\ k) . n < x0 by NAT_1:def 3;
x0 - r < s . (n + k) by A42, 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 A49;
then (s ^\ k) . n in ].(x0 - r),x0.[ by RCOMP_1:def 2;
then A50: (s ^\ k) . n in ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ by XBOOLE_0:def 3;
s . (n + k) in dom f2 by A38, A48;
then (s ^\ k) . n in dom f2 by NAT_1:def 3;
hence x in (dom f2) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) by A47, A50, XBOOLE_0:def 4; :: thesis: verum

end;

then A51: rng (s ^\ k) c= (dom f2) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) ;
then A52: rng (s ^\ k) c= (dom f1) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) by A32;

A53: 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
A54: 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 A32, A46;
then f1 . ((s ^\ k) . n) <= (f2 /* (s ^\ k)) . n by A51, FUNCT_2:108, XBOOLE_1:18, A54;
hence (f1 /* (s ^\ k)) . n <= (f2 /* (s ^\ k)) . n by A52, FUNCT_2:108, XBOOLE_1:18, A54; :: thesis: verum

end;

A55: rng (s ^\ k) c= dom f1 by A52, XBOOLE_1:18;
A56: rng (s ^\ k) c= (dom f1) \ {x0}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (s ^\ k) or x in (dom f1) \ {x0} )
assume A57: x in rng (s ^\ k) ; :: thesis: x in (dom f1) \ {x0}
then not x in {x0} by A44, XBOOLE_0:def 5;
hence x in (dom f1) \ {x0} by A55, A57, XBOOLE_0:def 5; :: thesis: verum

end;

then A58: lim (f1 /* (s ^\ k)) = lim (f1,x0) by A1, A41, A43, Def4;
A59: f1 /* (s ^\ k) is convergent by A1, A41, A43, A56;
f2 /* (s ^\ k) is convergent by A2, A41, A43, A44;
hence lim (f1,x0) <= lim (f2,x0) by A45, A59, A58, A53, SEQ_2:18; :: thesis: verum

end;

end;

end;

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