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 )
A3: lim f2,x0 = lim f2,x0 ;
given r being Real such that A4: 0 < r and
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 ) ) 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
A6: lim f1,x0 = lim f1,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 A5;
suppose A7: ( (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 S1[ 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 g1 being Real st S1[n,g1]
A9: x0 < x0 + 1 by Lm1;
x0 - (1 / (n + 1)) < x0 by Lm3;
then consider g1, g2 being Real such that
A10: x0 - (1 / (n + 1)) < g1 and
A11: g1 < x0 and
A12: g1 in dom f1 and
g2 < x0 + 1 and
x0 < g2 and
g2 in dom f1 by A1, A9, Def1;
take g1 = g1; :: thesis: S1[n,g1]
thus S1[n,g1] by A10, A11, A12; :: thesis: verum
end;
consider s being Real_Sequence such that
A13: for n being Element of NAT holds S1[n,s . n] from FUNCT_2:sch 3(A8);
A14: lim s = x0 by A13, Th6;
A15: rng s c= (dom f1) \ {x0} by A13, Th6;
A16: s is convergent by A13, Th6;
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, A14, LIMFUNC2:1;
A18: lim (s ^\ k) = x0 by A16, A14, SEQ_4:33;
rng (s ^\ k) c= rng s by VALUED_0:21;
then A19: rng (s ^\ k) c= (dom f1) \ {x0} by A15, XBOOLE_1:1;
then A20: lim (f1 /* (s ^\ k)) = lim f1,x0 by A1, A16, A18, 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
A21: (s ^\ k) . n = x by FUNCT_2:190;
s . (n + k) < x0 by A13;
then A22: (s ^\ k) . n < x0 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 A22;
then (s ^\ k) . n in ].(x0 - r),x0.[ by RCOMP_1:def 2;
then A23: (s ^\ k) . n in ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ by XBOOLE_0:def 3;
s . (n + k) in dom f1 by A13;
then (s ^\ k) . n in dom f1 by NAT_1:def 3;
hence x in (dom f1) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) by A21, A23, XBOOLE_0:def 4; :: thesis: verum
end;
then A24: rng (s ^\ k) c= (dom f1) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) by TARSKI:def 3;
then A25: rng (s ^\ k) c= (dom f2) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) by A7, XBOOLE_1:1;
A26: 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, A24;
then f1 . ((s ^\ k) . n) <= (f2 /* (s ^\ k)) . n by A25, FUNCT_2:185, XBOOLE_1:18;
hence (f1 /* (s ^\ k)) . n <= (f2 /* (s ^\ k)) . n by A24, FUNCT_2:185, XBOOLE_1:18; :: thesis: verum
end;
A27: rng (s ^\ k) c= dom f2 by A25, XBOOLE_1:18;
A28: 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 A29: x in rng (s ^\ k) ; :: thesis: x in (dom f2) \ {x0}
then not x in {x0} by A19, 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, A16, A18, Def4;
A31: f2 /* (s ^\ k) is convergent by A2, A3, A16, A18, A28, Def4;
f1 /* (s ^\ k) is convergent by A1, A6, A16, A18, A19, Def4;
hence lim f1,x0 <= lim f2,x0 by A20, A31, A30, A26, SEQ_2:32; :: 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 S1[ Element of NAT , real number ] means ( x0 - (1 / ($1 + 1)) < $2 & $2 < x0 & $2 in dom f2 );
A33: now
let n be Element of NAT ; :: thesis: ex g1 being Real st S1[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, Def1;
take g1 = g1; :: thesis: S1[n,g1]
thus S1[n,g1] by A35, A36, A37; :: thesis: verum
end;
consider s being Real_Sequence such that
A38: for n being Element of NAT holds S1[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 A4, Lm1;
then consider k being Element of NAT such that
A42: for n being Element of NAT st k <= n holds
x0 - r < s . n by A41, A39, LIMFUNC2:1;
A43: lim (s ^\ k) = x0 by A41, A39, SEQ_4:33;
rng (s ^\ k) c= rng s by VALUED_0:21;
then A44: rng (s ^\ k) c= (dom f2) \ {x0} by A40, XBOOLE_1:1;
then A45: lim (f2 /* (s ^\ k)) = lim f2,x0 by A2, A41, A43, Def4;
A46: 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
A47: (s ^\ k) . n = x by FUNCT_2:190;
s . (n + k) < x0 by A38;
then A48: (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 A48;
then (s ^\ k) . n in ].(x0 - r),x0.[ by RCOMP_1:def 2;
then A49: (s ^\ k) . n in ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ by XBOOLE_0:def 3;
s . (n + k) in dom f2 by A38;
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, A49, XBOOLE_0:def 4; :: thesis: verum
end;
then A50: rng (s ^\ k) c= (dom f2) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) by TARSKI:def 3;
then A51: rng (s ^\ k) c= (dom f1) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) by A32, XBOOLE_1:1;
A52: 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 A32, A46;
then f1 . ((s ^\ k) . n) <= (f2 /* (s ^\ k)) . n by A50, FUNCT_2:185, XBOOLE_1:18;
hence (f1 /* (s ^\ k)) . n <= (f2 /* (s ^\ k)) . n by A51, FUNCT_2:185, XBOOLE_1:18; :: thesis: verum
end;
A53: rng (s ^\ k) c= dom f1 by A51, XBOOLE_1:18;
A54: 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 A55: 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 A53, A55, XBOOLE_0:def 5; :: thesis: verum
end;
then A56: lim (f1 /* (s ^\ k)) = lim f1,x0 by A1, A41, A43, Def4;
A57: f1 /* (s ^\ k) is convergent by A1, A6, A41, A43, A54, Def4;
f2 /* (s ^\ k) is convergent by A2, A3, A41, A43, A44, Def4;
hence lim f1,x0 <= lim f2,x0 by A45, A57, A56, A52, SEQ_2:32; :: thesis: verum
end;
end;
end;
hence lim f1,x0 <= lim f2,x0 ; :: thesis: verum