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 A1: ( f1 is_convergent_in x0 & 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 A2: 0 < r and
A3: ( ( (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
A4: ( lim f1,x0 = lim f1,x0 & lim f2,x0 = lim f2,x0 ) ;

now

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

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

A6: now

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

end;

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

now

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

end;

then A18: rng (s ^\ k) c= (dom f1) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) by TARSKI:def 3;
then A19: rng (s ^\ k) c= (dom f2) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) by A5, XBOOLE_1:1;
then A20: rng (s ^\ k) c= dom f2 by XBOOLE_1:18;
rng (s ^\ k) c= (dom f2) \ {x0}

proof

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

end;

then A22: ( f2 /* (s ^\ k) is convergent & lim (f2 /* (s ^\ k)) = lim f2,x0 ) by A1, A4, A12, Def4;

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

end;

hence lim f1,x0 <= lim f2,x0 by A14, A22, SEQ_2:32; :: thesis: verum

end;

suppose A23: ( (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 number ] means ( x0 - (1 / ($1 + 1)) < $2 & $2 < x0 & $2 in dom f2 );

A24: now

let n be Element of NAT ; :: thesis: ex g1 being Real st S₁[n,g1]
A25: x0 - (1 / (n + 1)) < x0 by Lm3;
x0 < x0 + 1 by Lm1;
then consider g1, g2 being Real such that
A26: ( x0 - (1 / (n + 1)) < g1 & g1 < x0 & g1 in dom f2 & g2 < x0 + 1 & x0 < g2 & g2 in dom f2 ) by A1, A25, Def1;
take g1 = g1; :: thesis: S₁[n,g1]
thus S₁[n,g1] by A26; :: thesis: verum

end;

consider s being Real_Sequence such that
A27: for n being Element of NAT holds S₁[n,s . n] from FUNCT_2:sch 3(A24);
A28: ( s is convergent & lim s = x0 & rng s c= (dom f2) \ {x0} ) by A27, Th6;
x0 - r < x0 by A2, Lm1;
then consider k being Element of NAT such that
A29: for n being Element of NAT st k <= n holds
x0 - r < s . n by A28, LIMFUNC2:1;
A30: ( s ^\ k is convergent & lim (s ^\ k) = x0 ) by A28, SEQ_4:33;
rng (s ^\ k) c= rng s by VALUED_0:21;
then A31: rng (s ^\ k) c= (dom f2) \ {x0} by A28, XBOOLE_1:1;
then A32: ( f2 /* (s ^\ k) is convergent & lim (f2 /* (s ^\ k)) = lim f2,x0 ) by A1, A4, A30, Def4;

A33: now

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

end;

then A37: rng (s ^\ k) c= (dom f2) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) by TARSKI:def 3;
then A38: rng (s ^\ k) c= (dom f1) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) by A23, XBOOLE_1:1;
then A39: rng (s ^\ k) c= dom f1 by XBOOLE_1:18;
rng (s ^\ k) c= (dom f1) \ {x0}

proof

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

end;

then A41: ( f1 /* (s ^\ k) is convergent & lim (f1 /* (s ^\ k)) = lim f1,x0 ) by A1, A4, A30, Def4;

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

end;

hence lim f1,x0 <= lim f2,x0 by A32, A41, SEQ_2:32; :: thesis: verum

end;

end;

end;

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