let x0 be Real; :: thesis: for f being PartFunc of REAL ,REAL st f is_left_convergent_in x0 & f is_right_convergent_in x0 & lim_left f,x0 = lim_right f,x0 holds
( f is_convergent_in x0 & lim f,x0 = lim_left f,x0 & lim f,x0 = lim_right f,x0 )
let f be PartFunc of REAL ,REAL ; :: thesis: ( f is_left_convergent_in x0 & f is_right_convergent_in x0 & lim_left f,x0 = lim_right f,x0 implies ( f is_convergent_in x0 & lim f,x0 = lim_left f,x0 & lim f,x0 = lim_right f,x0 ) )
assume that
A1: f is_left_convergent_in x0 and
A2: f is_right_convergent_in x0 and
A3: lim_left f,x0 = lim_right f,x0 ; :: thesis: ( f is_convergent_in x0 & lim f,x0 = lim_left f,x0 & lim f,x0 = lim_right f,x0 )
A4: now
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_left f,x0 ) )
assume that
A5: s is convergent and
A6: lim s = x0 and
A7: rng s c= (dom f) \ {x0} ; :: thesis: ( f /* s is convergent & lim (f /* s) = lim_left f,x0 )
now
per cases ( ex k being Element of NAT st
for n being Element of NAT st k <= n holds
s . n < x0 or for k being Element of NAT ex n being Element of NAT st
( k <= n & s . n >= x0 ) ) ;
suppose ex k being Element of NAT st
for n being Element of NAT st k <= n holds
s . n < x0 ; :: thesis: ( f /* s is convergent & lim (f /* s) = lim_left f,x0 )
then consider k being Element of NAT such that
A8: for n being Element of NAT st k <= n holds
s . n < x0 ;
A9: rng s c= dom f by A7, XBOOLE_1:1;
A10: rng (s ^\ k) c= (dom f) /\ (left_open_halfline x0)
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (s ^\ k) or x in (dom f) /\ (left_open_halfline x0) )
assume x in rng (s ^\ k) ; :: thesis: x in (dom f) /\ (left_open_halfline x0)
then consider n being Element of NAT such that
A11: (s ^\ k) . n = x by FUNCT_2:190;
s . (n + k) < x0 by A8, NAT_1:12;
then s . (n + k) in { g1 where g1 is Real : g1 < x0 } ;
then s . (n + k) in left_open_halfline x0 by XXREAL_1:229;
then A12: x in left_open_halfline x0 by A11, NAT_1:def 3;
s . (n + k) in rng s by VALUED_0:28;
then x in rng s by A11, NAT_1:def 3;
hence x in (dom f) /\ (left_open_halfline x0) by A9, A12, XBOOLE_0:def 4; :: thesis: verum
end;
A13: f /* (s ^\ k) = (f /* s) ^\ k by A7, VALUED_0:27, XBOOLE_1:1;
A14: lim (s ^\ k) = x0 by A5, A6, SEQ_4:33;
then A15: f /* (s ^\ k) is convergent by A1, A3, A5, A10, LIMFUNC2:def 7;
hence f /* s is convergent by A13, SEQ_4:35; :: thesis: lim (f /* s) = lim_left f,x0
lim (f /* (s ^\ k)) = lim_left f,x0 by A1, A5, A14, A10, LIMFUNC2:def 7;
hence lim (f /* s) = lim_left f,x0 by A15, A13, SEQ_4:36; :: thesis: verum
end;
suppose A16: for k being Element of NAT ex n being Element of NAT st
( k <= n & s . n >= x0 ) ; :: thesis: ( f /* s is convergent & lim (f /* s) = lim_left f,x0 )
now
per cases ( ex k being Element of NAT st
for n being Element of NAT st k <= n holds
x0 < s . n or for k being Element of NAT ex n being Element of NAT st
( k <= n & x0 >= s . n ) ) ;
suppose ex k being Element of NAT st
for n being Element of NAT st k <= n holds
x0 < s . n ; :: thesis: ( f /* s is convergent & lim (f /* s) = lim_left f,x0 )
then consider k being Element of NAT such that
A17: for n being Element of NAT st k <= n holds
s . n > x0 ;
A18: rng s c= dom f by A7, XBOOLE_1:1;
A19: rng (s ^\ k) c= (dom f) /\ (right_open_halfline x0)
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (s ^\ k) or x in (dom f) /\ (right_open_halfline x0) )
assume x in rng (s ^\ k) ; :: thesis: x in (dom f) /\ (right_open_halfline x0)
then consider n being Element of NAT such that
A20: (s ^\ k) . n = x by FUNCT_2:190;
x0 < s . (n + k) by A17, NAT_1:12;
then s . (n + k) in { g1 where g1 is Real : x0 < g1 } ;
then s . (n + k) in right_open_halfline x0 by XXREAL_1:230;
then A21: x in right_open_halfline x0 by A20, NAT_1:def 3;
s . (n + k) in rng s by VALUED_0:28;
then x in rng s by A20, NAT_1:def 3;
hence x in (dom f) /\ (right_open_halfline x0) by A18, A21, XBOOLE_0:def 4; :: thesis: verum
end;
A22: f /* (s ^\ k) = (f /* s) ^\ k by A7, VALUED_0:27, XBOOLE_1:1;
A23: lim (s ^\ k) = x0 by A5, A6, SEQ_4:33;
then A24: f /* (s ^\ k) is convergent by A2, A3, A5, A19, LIMFUNC2:def 8;
hence f /* s is convergent by A22, SEQ_4:35; :: thesis: lim (f /* s) = lim_left f,x0
lim (f /* (s ^\ k)) = lim_left f,x0 by A2, A3, A5, A23, A19, LIMFUNC2:def 8;
hence lim (f /* s) = lim_left f,x0 by A24, A22, SEQ_4:36; :: thesis: verum
end;
suppose A25: for k being Element of NAT ex n being Element of NAT st
( k <= n & x0 >= s . n ) ; :: thesis: ( f /* s is convergent & lim (f /* s) = lim_left f,x0 )
set GR = lim_left f,x0;
defpred S1[ set , set ] means for n, m being Element of NAT st $1 = n & $2 = m holds
( n < m & s . m < x0 & ( for k being Element of NAT st n < k & s . k < x0 holds
m <= k ) );
defpred S2[ Element of NAT , set , set ] means S1[$2,$3];
defpred S3[ Nat] means s . $1 < x0;
A26: now
let k be Element of NAT ; :: thesis: ex n being Element of NAT st
( k <= n & s . n < x0 )
consider n being Element of NAT such that
A27: k <= n and
A28: s . n <= x0 by A25;
take n = n; :: thesis: ( k <= n & s . n < x0 )
thus k <= n by A27; :: thesis: s . n < x0
s . n in rng s by VALUED_0:28;
then not s . n in {x0} by A7, XBOOLE_0:def 5;
then s . n <> x0 by TARSKI:def 1;
hence s . n < x0 by A28, XXREAL_0:1; :: thesis: verum
end;
then ex m1 being Element of NAT st
( 0 <= m1 & s . m1 < x0 ) ;
then A29: ex m being Nat st S3[m] ;
consider M being Nat such that
A30: ( S3[M] & ( for n being Nat st S3[n] holds
M <= n ) ) from NAT_1:sch 5(A29);
reconsider M9 = M as Element of NAT by ORDINAL1:def 13;
A31: now
let n be Element of NAT ; :: thesis: ex m being Element of NAT st
( n < m & s . m < x0 )
consider m being Element of NAT such that
A32: n + 1 <= m and
A33: s . m < x0 by A26;
take m = m; :: thesis: ( n < m & s . m < x0 )
thus ( n < m & s . m < x0 ) by A32, A33, NAT_1:13; :: thesis: verum
end;
A34: for n, x being Element of NAT ex y being Element of NAT st S2[n,x,y]
proof
let n, x be Element of NAT ; :: thesis: ex y being Element of NAT st S2[n,x,y]
defpred S4[ Nat] means ( x < $1 & s . $1 < x0 );
ex m being Element of NAT st S4[m] by A31;
then A35: ex m being Nat st S4[m] ;
consider l being Nat such that
A36: ( S4[l] & ( for k being Nat st S4[k] holds
l <= k ) ) from NAT_1:sch 5(A35);
 take l ; :: thesis: ( l is Element of REAL & l is Element of NAT & S2[n,x,l] )
l in NAT by ORDINAL1:def 13;
hence ( l is Element of REAL & l is Element of NAT & S2[n,x,l] ) by A36; :: thesis: verum
end;
consider F being Function of NAT ,NAT such that
A37: ( F . 0 = M9 & ( for n being Element of NAT holds S2[n,F . n,F . (n + 1)] ) ) from RECDEF_1:sch 2(A34);
A38: rng F c= NAT by RELAT_1:def 19;
then A39: rng F c= REAL by XBOOLE_1:1;
A40: dom F = NAT by FUNCT_2:def 1;
then reconsider F = F as Real_Sequence by A39, RELSET_1:11;
A41: now
let n be Element of NAT ; :: thesis: F . n is Element of NAT
F . n in rng F by A40, FUNCT_1:def 5;
hence F . n is Element of NAT by A38; :: thesis: verum
end;
now
let n be Element of NAT ; :: thesis: F . n < F . (n + 1)
A42: F . (n + 1) is Element of NAT by A41;
F . n is Element of NAT by A41;
hence F . n < F . (n + 1) by A37, A42; :: thesis: verum
end;
then reconsider F = F as V33() sequence of NAT by SEQM_3:def 11;
A43: s * F is subsequence of s by VALUED_0:def 17;
then rng (s * F) c= rng s by VALUED_0:21;
then A44: rng (s * F) c= (dom f) \ {x0} by A7, XBOOLE_1:1;
defpred S4[ Nat] means ( s . $1 < x0 & ( for m being Element of NAT holds F . m <> $1 ) );
A45: for n being Element of NAT st s . n < x0 holds
ex m being Element of NAT st F . m = n
proof
assume ex n being Element of NAT st S4[n] ; :: thesis: contradiction
then A46: ex n being Nat st S4[n] ;
consider M1 being Nat such that
A47: ( S4[M1] & ( for n being Nat st S4[n] holds
M1 <= n ) ) from NAT_1:sch 5(A46);
 defpred S5[ Nat] means ( $1 < M1 & s . $1 < x0 & ex m being Element of NAT st F . m = $1 );
A48: ex n being Nat st S5[n]
proof
take M ; :: thesis: S5[M]
A49: M <> M1 by A37, A47;
M <= M1 by A30, A47;
hence M < M1 by A49, XXREAL_0:1; :: thesis: ( s . M < x0 & ex m being Element of NAT st F . m = M )
thus s . M < x0 by A30; :: thesis: ex m being Element of NAT st F . m = M
take 0 ; :: thesis: F . 0 = M
thus F . 0 = M by A37; :: thesis: verum
end;
A50: for n being Nat st S5[n] holds
n <= M1 ;
consider MX being Nat such that
A51: ( S5[MX] & ( for n being Nat st S5[n] holds
n <= MX ) ) from NAT_1:sch 6(A50, A48);
 A52: for k being Element of NAT st MX < k & k < M1 holds
s . k >= x0
proof
given k being Element of NAT such that A53: MX < k and
A54: k < M1 and
A55: s . k < x0 ; :: thesis: contradiction
now
per cases ( ex m being Element of NAT st F . m = k or for m being Element of NAT holds F . m <> k ) ;
end;
end;
hence contradiction ; :: thesis: verum
end;
consider m being Element of NAT such that
A56: F . m = MX by A51;
M1 in NAT by ORDINAL1:def 13;
then A57: F . (m + 1) <= M1 by A37, A47, A51, A56;
A58: s . (F . (m + 1)) < x0 by A37, A56;
A59: MX < F . (m + 1) by A37, A56;
now
assume F . (m + 1) <> M1 ; :: thesis: contradiction
then F . (m + 1) < M1 by A57, XXREAL_0:1;
hence contradiction by A52, A59, A58; :: thesis: verum
end;
hence contradiction by A47; :: thesis: verum
end;
defpred S5[ Nat] means s . $1 > x0;
A60: now
let k be Element of NAT ; :: thesis: ex n being Element of NAT st
( k <= n & s . n > x0 )
consider n being Element of NAT such that
A61: k <= n and
A62: s . n >= x0 by A16;
take n = n; :: thesis: ( k <= n & s . n > x0 )
thus k <= n by A61; :: thesis: s . n > x0
s . n in rng s by VALUED_0:28;
then not s . n in {x0} by A7, XBOOLE_0:def 5;
then s . n <> x0 by TARSKI:def 1;
hence s . n > x0 by A62, XXREAL_0:1; :: thesis: verum
end;
then ex mn being Element of NAT st
( 0 <= mn & s . mn > x0 ) ;
then A63: ex m being Nat st S5[m] ;
consider N being Nat such that
A64: ( S5[N] & ( for n being Nat st S5[n] holds
N <= n ) ) from NAT_1:sch 5(A63);
A65: for n being Element of NAT holds (s * F) . n < x0
proof
defpred S6[ Element of NAT ] means (s * F) . $1 < x0;
A66: for k being Element of NAT st S6[k] holds
S6[k + 1]
proof
let k be Element of NAT ; :: thesis: ( S6[k] implies S6[k + 1] )
assume (s * F) . k < x0 ; :: thesis: S6[k + 1]
S1[F . k,F . (k + 1)] by A37;
then s . (F . (k + 1)) < x0 ;
hence S6[k + 1] by FUNCT_2:21; :: thesis: verum
end;
A67: S6[ 0 ] by A30, A37, FUNCT_2:21;
thus for k being Element of NAT holds S6[k] from NAT_1:sch 1(A67, A66); :: thesis: verum
end;
A68: rng (s * F) c= (dom f) /\ (left_open_halfline x0)
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (s * F) or x in (dom f) /\ (left_open_halfline x0) )
assume A69: x in rng (s * F) ; :: thesis: x in (dom f) /\ (left_open_halfline x0)
then consider n being Element of NAT such that
A70: (s * F) . n = x by FUNCT_2:190;
(s * F) . n < x0 by A65;
then x in { g1 where g1 is Real : g1 < x0 } by A70;
then A71: x in left_open_halfline x0 by XXREAL_1:229;
x in dom f by A44, A69, XBOOLE_0:def 5;
hence x in (dom f) /\ (left_open_halfline x0) by A71, XBOOLE_0:def 4; :: thesis: verum
end;
defpred S6[ set , set ] means for n, m being Element of NAT st $1 = n & $2 = m holds
( n < m & s . m > x0 & ( for k being Element of NAT st n < k & s . k > x0 holds
m <= k ) );
defpred S7[ Element of NAT , set , set ] means S6[$2,$3];
A72: s * F is convergent by A5, A43, SEQ_4:29;
reconsider N9 = N as Element of NAT by ORDINAL1:def 13;
A73: now
let n be Element of NAT ; :: thesis: ex m being Element of NAT st
( n < m & s . m > x0 )
consider m being Element of NAT such that
A74: n + 1 <= m and
A75: s . m > x0 by A60;
take m = m; :: thesis: ( n < m & s . m > x0 )
thus ( n < m & s . m > x0 ) by A74, A75, NAT_1:13; :: thesis: verum
end;
A76: for n, x being Element of NAT ex y being Element of NAT st S7[n,x,y]
proof
let n, x be Element of NAT ; :: thesis: ex y being Element of NAT st S7[n,x,y]
defpred S8[ Nat] means ( x < $1 & s . $1 > x0 );
ex m being Element of NAT st S8[m] by A73;
then A77: ex m being Nat st S8[m] ;
consider l being Nat such that
A78: ( S8[l] & ( for k being Nat st S8[k] holds
l <= k ) ) from NAT_1:sch 5(A77);
 take l ; :: thesis: ( l is Element of REAL & l is Element of NAT & S7[n,x,l] )
l in NAT by ORDINAL1:def 13;
hence ( l is Element of REAL & l is Element of NAT & S7[n,x,l] ) by A78; :: thesis: verum
end;
consider G being Function of NAT ,NAT such that
A79: ( G . 0 = N9 & ( for n being Element of NAT holds S7[n,G . n,G . (n + 1)] ) ) from RECDEF_1:sch 2(A76);
A80: rng G c= NAT by RELAT_1:def 19;
then A81: rng G c= REAL by XBOOLE_1:1;
A82: dom G = NAT by FUNCT_2:def 1;
then reconsider G = G as Real_Sequence by A81, RELSET_1:11;
A83: now
let n be Element of NAT ; :: thesis: G . n is Element of NAT
G . n in rng G by A82, FUNCT_1:def 5;
hence G . n is Element of NAT by A80; :: thesis: verum
end;
now
let n be Element of NAT ; :: thesis: G . n < G . (n + 1)
A84: G . (n + 1) is Element of NAT by A83;
G . n is Element of NAT by A83;
hence G . n < G . (n + 1) by A79, A84; :: thesis: verum
end;
then reconsider G = G as V33() sequence of NAT by SEQM_3:def 11;
A85: s * G is subsequence of s by VALUED_0:def 17;
then rng (s * G) c= rng s by VALUED_0:21;
then A86: rng (s * G) c= (dom f) \ {x0} by A7, XBOOLE_1:1;
A87: lim (s * F) = x0 by A5, A6, A43, SEQ_4:30;
then A88: lim (f /* (s * F)) = lim_left f,x0 by A1, A72, A68, LIMFUNC2:def 7;
A89: f /* (s * F) is convergent by A1, A3, A72, A87, A68, LIMFUNC2:def 7;
A90: s * G is convergent by A5, A85, SEQ_4:29;
defpred S8[ Nat] means ( s . $1 > x0 & ( for m being Element of NAT holds G . m <> $1 ) );
A91: for n being Element of NAT st s . n > x0 holds
ex m being Element of NAT st G . m = n
proof
assume ex n being Element of NAT st S8[n] ; :: thesis: contradiction
then A92: ex n being Nat st S8[n] ;
consider N1 being Nat such that
A93: ( S8[N1] & ( for n being Nat st S8[n] holds
N1 <= n ) ) from NAT_1:sch 5(A92);
 defpred S9[ Nat] means ( $1 < N1 & s . $1 > x0 & ex m being Element of NAT st G . m = $1 );
A94: ex n being Nat st S9[n]
proof
take N ; :: thesis: S9[N]
A95: N <> N1 by A79, A93;
N <= N1 by A64, A93;
hence N < N1 by A95, XXREAL_0:1; :: thesis: ( s . N > x0 & ex m being Element of NAT st G . m = N )
thus s . N > x0 by A64; :: thesis: ex m being Element of NAT st G . m = N
take 0 ; :: thesis: G . 0 = N
thus G . 0 = N by A79; :: thesis: verum
end;
A96: for n being Nat st S9[n] holds
n <= N1 ;
consider NX being Nat such that
A97: ( S9[NX] & ( for n being Nat st S9[n] holds
n <= NX ) ) from NAT_1:sch 6(A96, A94);
 A98: for k being Element of NAT st NX < k & k < N1 holds
s . k <= x0
proof
given k being Element of NAT such that A99: NX < k and
A100: k < N1 and
A101: s . k > x0 ; :: thesis: contradiction
now
per cases ( ex m being Element of NAT st G . m = k or for m being Element of NAT holds G . m <> k ) ;
end;
end;
hence contradiction ; :: thesis: verum
end;
consider m being Element of NAT such that
A102: G . m = NX by A97;
N1 in NAT by ORDINAL1:def 13;
then A103: G . (m + 1) <= N1 by A79, A93, A97, A102;
A104: s . (G . (m + 1)) > x0 by A79, A102;
A105: NX < G . (m + 1) by A79, A102;
now
assume G . (m + 1) <> N1 ; :: thesis: contradiction
then G . (m + 1) < N1 by A103, XXREAL_0:1;
hence contradiction by A98, A105, A104; :: thesis: verum
end;
hence contradiction by A93; :: thesis: verum
end;
A106: for n being Element of NAT holds (s * G) . n > x0
proof
defpred S9[ Element of NAT ] means (s * G) . $1 > x0;
A107: for k being Element of NAT st S9[k] holds
S9[k + 1]
proof
let k be Element of NAT ; :: thesis: ( S9[k] implies S9[k + 1] )
assume (s * G) . k > x0 ; :: thesis: S9[k + 1]
S6[G . k,G . (k + 1)] by A79;
then s . (G . (k + 1)) > x0 ;
hence S9[k + 1] by FUNCT_2:21; :: thesis: verum
end;
A108: S9[ 0 ] by A64, A79, FUNCT_2:21;
thus for k being Element of NAT holds S9[k] from NAT_1:sch 1(A108, A107); :: thesis: verum
end;
A109: rng (s * G) c= (dom f) /\ (right_open_halfline x0)
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (s * G) or x in (dom f) /\ (right_open_halfline x0) )
assume A110: x in rng (s * G) ; :: thesis: x in (dom f) /\ (right_open_halfline x0)
then consider n being Element of NAT such that
A111: (s * G) . n = x by FUNCT_2:190;
(s * G) . n > x0 by A106;
then x in { g1 where g1 is Real : x0 < g1 } by A111;
then A112: x in right_open_halfline x0 by XXREAL_1:230;
x in dom f by A86, A110, XBOOLE_0:def 5;
hence x in (dom f) /\ (right_open_halfline x0) by A112, XBOOLE_0:def 4; :: thesis: verum
end;
A113: lim (s * G) = x0 by A5, A6, A85, SEQ_4:30;
then A114: lim (f /* (s * G)) = lim_left f,x0 by A2, A3, A90, A109, LIMFUNC2:def 8;
A115: f /* (s * G) is convergent by A2, A3, A90, A113, A109, LIMFUNC2:def 8;
A116: now
let r be real number ; :: thesis: ( 0 < r implies ex n being Element of NAT st
for k being Element of NAT st n <= k holds
abs (((f /* s) . k) - (lim_left f,x0)) < r )
assume A117: 0 < r ; :: thesis: ex n being Element of NAT st
for k being Element of NAT st n <= k holds
abs (((f /* s) . k) - (lim_left f,x0)) < r
then consider n1 being Element of NAT such that
A118: for k being Element of NAT st n1 <= k holds
abs (((f /* (s * F)) . k) - (lim_left f,x0)) < r by A89, A88, SEQ_2:def 7;
consider n2 being Element of NAT such that
A119: for k being Element of NAT st n2 <= k holds
abs (((f /* (s * G)) . k) - (lim_left f,x0)) < r by A115, A114, A117, SEQ_2:def 7;
take n = max (F . n1),(G . n2); :: thesis: for k being Element of NAT st n <= k holds
abs (((f /* s) . k) - (lim_left f,x0)) < r
let k be Element of NAT ; :: thesis: ( n <= k implies abs (((f /* s) . k) - (lim_left f,x0)) < r )
assume A120: n <= k ; :: thesis: abs (((f /* s) . k) - (lim_left f,x0)) < r
s . k in rng s by VALUED_0:28;
then not s . k in {x0} by A7, XBOOLE_0:def 5;
then A121: s . k <> x0 by TARSKI:def 1;
now
per cases ( s . k < x0 or s . k > x0 ) by A121, XXREAL_0:1;
suppose s . k < x0 ; :: thesis: abs (((f /* s) . k) - (lim_left f,x0)) < r
then consider l being Element of NAT such that
A122: k = F . l by A45;
F . n1 <= n by XXREAL_0:25;
then F . n1 <= k by A120, XXREAL_0:2;
then l >= n1 by A122, SEQM_3:7;
then abs (((f /* (s * F)) . l) - (lim_left f,x0)) < r by A118;
then abs ((f . ((s * F) . l)) - (lim_left f,x0)) < r by A44, FUNCT_2:185, XBOOLE_1:1;
then abs ((f . (s . k)) - (lim_left f,x0)) < r by A122, FUNCT_2:21;
hence abs (((f /* s) . k) - (lim_left f,x0)) < r by A7, FUNCT_2:185, XBOOLE_1:1; :: thesis: verum
end;
suppose s . k > x0 ; :: thesis: abs (((f /* s) . k) - (lim_left f,x0)) < r
then consider l being Element of NAT such that
A123: k = G . l by A91;
G . n2 <= n by XXREAL_0:25;
then G . n2 <= k by A120, XXREAL_0:2;
then l >= n2 by A123, SEQM_3:7;
then abs (((f /* (s * G)) . l) - (lim_left f,x0)) < r by A119;
then abs ((f . ((s * G) . l)) - (lim_left f,x0)) < r by A86, FUNCT_2:185, XBOOLE_1:1;
then abs ((f . (s . k)) - (lim_left f,x0)) < r by A123, FUNCT_2:21;
hence abs (((f /* s) . k) - (lim_left f,x0)) < r by A7, FUNCT_2:185, XBOOLE_1:1; :: thesis: verum
end;
end;
end;
hence abs (((f /* s) . k) - (lim_left f,x0)) < r ; :: thesis: verum
end;
hence f /* s is convergent by SEQ_2:def 6; :: thesis: lim (f /* s) = lim_left f,x0
hence lim (f /* s) = lim_left f,x0 by A116, SEQ_2:def 7; :: thesis: verum
end;
end;
end;
hence ( f /* s is convergent & lim (f /* s) = lim_left f,x0 ) ; :: thesis: verum
end;
end;
end;
hence ( f /* s is convergent & lim (f /* s) = lim_left f,x0 ) ; :: thesis: verum
end;
now
let r1, r2 be Real; :: thesis: ( r1 < x0 & x0 < r2 implies ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) )
assume that
A124: r1 < x0 and
A125: x0 < r2 ; :: thesis: ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f )
consider g1 being Real such that
A126: r1 < g1 and
A127: g1 < x0 and
A128: g1 in dom f by A1, A124, LIMFUNC2:def 1;
consider g2 being Real such that
A129: g2 < r2 and
A130: x0 < g2 and
A131: g2 in dom f by A2, A125, LIMFUNC2:def 4;
take g1 = g1; :: thesis: ex g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f )
take g2 = g2; :: thesis: ( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f )
thus ( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) by A126, A127, A128, A129, A130, A131; :: thesis: verum
end;
hence f is_convergent_in x0 by A4, Def1; :: thesis: ( lim f,x0 = lim_left f,x0 & lim f,x0 = lim_right f,x0 )
hence ( lim f,x0 = lim_left f,x0 & lim f,x0 = lim_right f,x0 ) by A3, A4, Def4; :: thesis: verum