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

now :: thesis: ( f is_convergent_in x0 & f is_convergent_in x0 & lim (f,x0) = lim (f1,x0) )

per cases ( ( (dom f1) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[) c= (dom f2) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[) & (dom f) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[) c= (dom f1) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[) ) or ( (dom f2) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[) c= (dom f1) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[) & (dom f) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[) c= (dom f2) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[) ) ) by A7;

suppose A8: ( (dom f1) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[) c= (dom f2) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[) & (dom f) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[) c= (dom f1) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[) ) ; :: thesis: ( f is_convergent_in x0 & f is_convergent_in x0 & lim (f,x0) = lim (f1,x0) )

A9: now :: thesis: for s being Real_Sequence st s is convergent & lim s = x0 & rng s c= (dom f) \ {x0} holds
( f /* s is convergent & lim (f /* s) = lim (f1,x0) )

let s be Real_Sequence; :: thesis: ( s is convergent & lim s = x0 & rng s c= (dom f) \ {x0} implies ( f /* s is convergent & lim (f /* s) = lim (f1,x0) ) )
assume that
A10: s is convergent and
A11: lim s = x0 and
A12: rng s c= (dom f) \ {x0} ; :: thesis: ( f /* s is convergent & lim (f /* s) = lim (f1,x0) )
consider k being Element of NAT such that
A13: for n being Element of NAT st k <= n holds
( x0 - r1 < s . n & s . n < x0 + r1 ) by A5, A10, A11, Th7;
A14: rng (s ^\ k) c= rng s by VALUED_0:21;
then A15: rng (s ^\ k) c= (dom f) \ {x0} by A12;

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

let x be object ; :: thesis: ( x in rng (s ^\ k) implies x in ].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[ )
assume A16: x in rng (s ^\ k) ; :: thesis: x in ].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[
then consider n being Element of NAT such that
A17: x = (s ^\ k) . n by FUNCT_2:113;
A18: k <= n + k by NAT_1:12;
then s . (n + k) < x0 + r1 by A13;
then A19: (s ^\ k) . n < x0 + r1 by NAT_1:def 3;
x0 - r1 < s . (n + k) by A13, A18;
then x0 - r1 < (s ^\ k) . n by NAT_1:def 3;
then (s ^\ k) . n in { g1 where g1 is Real : ( x0 - r1 < g1 & g1 < x0 + r1 ) } by A19;
then A20: (s ^\ k) . n in ].(x0 - r1),(x0 + r1).[ by RCOMP_1:def 2;
not (s ^\ k) . n in {x0} by A15, A16, A17, XBOOLE_0:def 5;
then x in ].(x0 - r1),(x0 + r1).[ \ {x0} by A17, A20, XBOOLE_0:def 5;
hence x in ].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[ by A5, Th4; :: thesis: verum

end;

then A21: rng (s ^\ k) c= ].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[ ;
A22: rng s c= dom f by A12, XBOOLE_1:1;
then rng (s ^\ k) c= dom f by A14;
then A23: rng (s ^\ k) c= (dom f) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[) by A21, XBOOLE_1:19;
then A24: rng (s ^\ k) c= (dom f1) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[) by A8;
then A25: rng (s ^\ k) c= (dom f2) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[) by A8;
A26: lim (s ^\ k) = x0 by A10, A11, SEQ_4:20;
A27: (dom f2) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[) c= dom f2 by XBOOLE_1:17;
then A28: rng (s ^\ k) c= dom f2 by A25;
A29: 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 A30: x in rng (s ^\ k) ; :: thesis: x in (dom f2) \ {x0}
then not x in {x0} by A15, XBOOLE_0:def 5;
hence x in (dom f2) \ {x0} by A28, A30, XBOOLE_0:def 5; :: thesis: verum

end;

then A31: lim (f2 /* (s ^\ k)) = lim (f2,x0) by A2, A10, A26, Def4;
A32: (dom f1) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[) c= dom f1 by XBOOLE_1:17;
then A33: rng (s ^\ k) c= dom f1 by A24;
A34: 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 A35: x in rng (s ^\ k) ; :: thesis: x in (dom f1) \ {x0}
then not x in {x0} by A15, XBOOLE_0:def 5;
hence x in (dom f1) \ {x0} by A33, A35, XBOOLE_0:def 5; :: thesis: verum

end;

then A36: lim (f1 /* (s ^\ k)) = lim (f1,x0) by A1, A10, A26, Def4;

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

let n be Nat; :: thesis: ( (f1 /* (s ^\ k)) . n <= (f /* (s ^\ k)) . n & (f /* (s ^\ k)) . n <= (f2 /* (s ^\ k)) . n )
A38: n in NAT by ORDINAL1:def 12;
A39: (s ^\ k) . n in rng (s ^\ k) by VALUED_0:28;
then f . ((s ^\ k) . n) <= f2 . ((s ^\ k) . n) by A6, A23;
then A40: (f /* (s ^\ k)) . n <= f2 . ((s ^\ k) . n) by A14, A22, FUNCT_2:108, XBOOLE_1:1, A38;
f1 . ((s ^\ k) . n) <= f . ((s ^\ k) . n) by A6, A23, A39;
then f1 . ((s ^\ k) . n) <= (f /* (s ^\ k)) . n by A14, A22, FUNCT_2:108, XBOOLE_1:1, A38;
hence ( (f1 /* (s ^\ k)) . n <= (f /* (s ^\ k)) . n & (f /* (s ^\ k)) . n <= (f2 /* (s ^\ k)) . n ) by A32, A27, A24, A25, A40, FUNCT_2:108, XBOOLE_1:1, A38; :: thesis: verum

end;

A41: f2 /* (s ^\ k) is convergent by A2, A10, A26, A29;
A42: f1 /* (s ^\ k) is convergent by A1, A10, A26, A34;
then f /* (s ^\ k) is convergent by A3, A36, A41, A31, A37, SEQ_2:19;
then A43: (f /* s) ^\ k is convergent by A12, VALUED_0:27, XBOOLE_1:1;
hence f /* s is convergent by SEQ_4:21; :: thesis: lim (f /* s) = lim (f1,x0)
lim (f /* (s ^\ k)) = lim (f1,x0) by A3, A42, A36, A41, A31, A37, SEQ_2:20;
then lim ((f /* s) ^\ k) = lim (f1,x0) by A12, VALUED_0:27, XBOOLE_1:1;
hence lim (f /* s) = lim (f1,x0) by A43, SEQ_4:22; :: thesis: verum

end;

hence f is_convergent_in x0 by A4; :: thesis: ( f is_convergent_in x0 & lim (f,x0) = lim (f1,x0) )
hence ( f is_convergent_in x0 & lim (f,x0) = lim (f1,x0) ) by A9, Def4; :: thesis: verum

end;

suppose A44: ( (dom f2) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[) c= (dom f1) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[) & (dom f) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[) c= (dom f2) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[) ) ; :: thesis: ( f is_convergent_in x0 & f is_convergent_in x0 & lim (f,x0) = lim (f1,x0) )

A45: now :: thesis: for s being Real_Sequence st s is convergent & lim s = x0 & rng s c= (dom f) \ {x0} holds
( f /* s is convergent & lim (f /* s) = lim (f1,x0) )

let s be Real_Sequence; :: thesis: ( s is convergent & lim s = x0 & rng s c= (dom f) \ {x0} implies ( f /* s is convergent & lim (f /* s) = lim (f1,x0) ) )
assume that
A46: s is convergent and
A47: lim s = x0 and
A48: rng s c= (dom f) \ {x0} ; :: thesis: ( f /* s is convergent & lim (f /* s) = lim (f1,x0) )
consider k being Element of NAT such that
A49: for n being Element of NAT st k <= n holds
( x0 - r1 < s . n & s . n < x0 + r1 ) by A5, A46, A47, Th7;
A50: rng (s ^\ k) c= rng s by VALUED_0:21;
then A51: rng (s ^\ k) c= (dom f) \ {x0} by A48;

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

let x be object ; :: thesis: ( x in rng (s ^\ k) implies x in ].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[ )
assume A52: x in rng (s ^\ k) ; :: thesis: x in ].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[
then consider n being Element of NAT such that
A53: x = (s ^\ k) . n by FUNCT_2:113;
A54: k <= n + k by NAT_1:12;
then s . (n + k) < x0 + r1 by A49;
then A55: (s ^\ k) . n < x0 + r1 by NAT_1:def 3;
x0 - r1 < s . (n + k) by A49, A54;
then x0 - r1 < (s ^\ k) . n by NAT_1:def 3;
then (s ^\ k) . n in { g1 where g1 is Real : ( x0 - r1 < g1 & g1 < x0 + r1 ) } by A55;
then A56: (s ^\ k) . n in ].(x0 - r1),(x0 + r1).[ by RCOMP_1:def 2;
not (s ^\ k) . n in {x0} by A51, A52, A53, XBOOLE_0:def 5;
then x in ].(x0 - r1),(x0 + r1).[ \ {x0} by A53, A56, XBOOLE_0:def 5;
hence x in ].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[ by A5, Th4; :: thesis: verum

end;

then A57: rng (s ^\ k) c= ].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[ ;
A58: rng s c= dom f by A48, XBOOLE_1:1;
then rng (s ^\ k) c= dom f by A50;
then A59: rng (s ^\ k) c= (dom f) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[) by A57, XBOOLE_1:19;
then A60: rng (s ^\ k) c= (dom f2) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[) by A44;
then A61: rng (s ^\ k) c= (dom f1) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[) by A44;
A62: lim (s ^\ k) = x0 by A46, A47, SEQ_4:20;
A63: (dom f2) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[) c= dom f2 by XBOOLE_1:17;
then A64: rng (s ^\ k) c= dom f2 by A60;
A65: 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 A66: x in rng (s ^\ k) ; :: thesis: x in (dom f2) \ {x0}
then not x in {x0} by A51, XBOOLE_0:def 5;
hence x in (dom f2) \ {x0} by A64, A66, XBOOLE_0:def 5; :: thesis: verum

end;

then A67: lim (f2 /* (s ^\ k)) = lim (f2,x0) by A2, A46, A62, Def4;
A68: (dom f1) /\ (].(x0 - r1),x0.[ \/ ].x0,(x0 + r1).[) c= dom f1 by XBOOLE_1:17;
then A69: rng (s ^\ k) c= dom f1 by A61;
A70: 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 A71: x in rng (s ^\ k) ; :: thesis: x in (dom f1) \ {x0}
then not x in {x0} by A51, XBOOLE_0:def 5;
hence x in (dom f1) \ {x0} by A69, A71, XBOOLE_0:def 5; :: thesis: verum

end;

then A72: lim (f1 /* (s ^\ k)) = lim (f1,x0) by A1, A46, A62, Def4;

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

let n be Nat; :: thesis: ( (f1 /* (s ^\ k)) . n <= (f /* (s ^\ k)) . n & (f /* (s ^\ k)) . n <= (f2 /* (s ^\ k)) . n )
A74: n in NAT by ORDINAL1:def 12;
A75: (s ^\ k) . n in rng (s ^\ k) by VALUED_0:28;
then f . ((s ^\ k) . n) <= f2 . ((s ^\ k) . n) by A6, A59;
then A76: (f /* (s ^\ k)) . n <= f2 . ((s ^\ k) . n) by A50, A58, FUNCT_2:108, XBOOLE_1:1, A74;
f1 . ((s ^\ k) . n) <= f . ((s ^\ k) . n) by A6, A59, A75;
then f1 . ((s ^\ k) . n) <= (f /* (s ^\ k)) . n by A50, A58, FUNCT_2:108, XBOOLE_1:1, A74;
hence ( (f1 /* (s ^\ k)) . n <= (f /* (s ^\ k)) . n & (f /* (s ^\ k)) . n <= (f2 /* (s ^\ k)) . n ) by A68, A63, A60, A61, A76, FUNCT_2:108, XBOOLE_1:1, A74; :: thesis: verum

end;

A77: f2 /* (s ^\ k) is convergent by A2, A46, A62, A65;
A78: f1 /* (s ^\ k) is convergent by A1, A46, A62, A70;
then f /* (s ^\ k) is convergent by A3, A72, A77, A67, A73, SEQ_2:19;
then A79: (f /* s) ^\ k is convergent by A48, VALUED_0:27, XBOOLE_1:1;
hence f /* s is convergent by SEQ_4:21; :: thesis: lim (f /* s) = lim (f1,x0)
lim (f /* (s ^\ k)) = lim (f1,x0) by A3, A78, A72, A77, A67, A73, SEQ_2:20;
then lim ((f /* s) ^\ k) = lim (f1,x0) by A48, VALUED_0:27, XBOOLE_1:1;
hence lim (f /* s) = lim (f1,x0) by A79, SEQ_4:22; :: thesis: verum

end;

hence f is_convergent_in x0 by A4; :: thesis: ( f is_convergent_in x0 & lim (f,x0) = lim (f1,x0) )
hence ( f is_convergent_in x0 & lim (f,x0) = lim (f1,x0) ) by A45, Def4; :: thesis: verum

end;

end;

end;

hence ( f is_convergent_in x0 & lim (f,x0) = lim (f1,x0) ) ; :: thesis: verum