let x0 be Real; :: thesis:
let f be PartFunc of REAL,REAL; :: thesis:

hereby :: thesis:

assume A1: f is_Rcontinuous_in x0 ; :: thesis:
hence x0 in dom f by FDIFF_3:def 2; :: thesis:
given e being Real such that A2: 0 < e and
A3: for d being Real holds
( not 0 < d or ex x1 being Real st
( x1 in dom f & x0 < x1 & x1 < x0 + d & not |.((f . x1) - (f . x0)).| < e ) ) ; :: thesis:
defpred S₁[ Element of NAT , Real] means ( $2 in dom f & x0 < $2 & $2 < x0 + (1 / ($1 + 1)) & not |.((f . $2) - (f . x0)).| < e );
A4: for n being Element of NAT ex p being Element of REAL st S₁[n,p]

proof

let n be Element of NAT ; :: thesis:
ex p being Real st
( p in dom f & x0 < p & p < x0 + (1 / (n + 1)) & not |.((f . p) - (f . x0)).| < e ) by A3;
hence ex p being Element of REAL st S₁[n,p] ; :: thesis:

end;

consider s1 being Real_Sequence such that
A5: for n being Element of NAT holds S₁[n,s1 . n] from FUNCT_2:sch 3(A4);

now :: thesis:

let x be Real; :: thesis:
assume x in rng s1 ; :: thesis:
then consider n being Element of NAT such that
A6: x = s1 . n by FUNCT_2:113;
A7: x in dom f by A5, A6;
x in ].x0,+infty.[ by A5, A6, XXREAL_1:235;
then x in right_open_halfline x0 by LIMFUNC1:def 3;
hence x in (right_open_halfline x0) /\ (dom f) by A7, XBOOLE_0:def 4; :: thesis:

end;

then A8: rng s1 c= (right_open_halfline x0) /\ (dom f) ;

A9: now :: thesis:

let n be Nat; :: thesis:
A10: n in NAT by ORDINAL1:def 12;
then A11: n in dom s1 by FUNCT_2:def 1;
A12: f /* s1 = f * s1 by A8, XBOOLE_1:18, FUNCT_2:def 11;
not |.((f . (s1 . n)) - (f . x0)).| < e by A5, A10;
hence not |.(((f /* s1) . n) - (f . x0)).| < e by FUNCT_1:13, A11, A12; :: thesis:

end;

A13: now :: thesis:

let d be Real; :: thesis:
assume A14: 0 < d ; :: thesis:
consider n being Nat such that
A15: d " < n by SEQ_4:3;
(d ") + 0 < n + 1 by A15, XREAL_1:8;
then A16: 1 / (n + 1) < 1 / (d ") by A14, XREAL_1:76;
take k = n; :: thesis:
let m be Nat; :: thesis:
A17: m in NAT by ORDINAL1:def 12;
assume k <= m ; :: thesis:
then k + 1 <= m + 1 by XREAL_1:6;
then 1 / (m + 1) <= 1 / (k + 1) by XREAL_1:118;
then A18: 1 / (m + 1) < d by A16, XXREAL_0:2;
( x0 < s1 . m & s1 . m < x0 + (1 / (m + 1)) ) by A5, A17;
then A19: ( (s1 . m) - x0 < 1 / (m + 1) & 0 < (s1 . m) - x0 ) by XREAL_1:19, XREAL_1:50;
then |.((s1 . m) - x0).| = (s1 . m) - x0 by ABSVALUE:def 1;
hence |.((s1 . m) - x0).| < d by A18, A19, XXREAL_0:2; :: thesis:

end;

then A20: s1 is convergent by SEQ_2:def 6;
then lim s1 = x0 by A13, SEQ_2:def 7;
then ( f /* s1 is convergent & f . x0 = lim (f /* s1) ) by A1, A8, A20, FDIFF_3:def 2;
then consider n being Nat such that
A21: for m being Nat st n <= m holds
|.(((f /* s1) . m) - (f . x0)).| < e by A2, SEQ_2:def 7;
|.(((f /* s1) . n) - (f . x0)).| < e by A21;
hence contradiction by A9; :: thesis:

end;

assume A22: ( x0 in dom f & ( for e being Real st 0 < e holds
ex d being Real st
( 0 < d & ( for x being Real st x in dom f & x0 < x & x < x0 + d holds
|.((f . x) - (f . x0)).| < e ) ) ) ) ; :: thesis:

now :: thesis:

let s1 be Real_Sequence; :: thesis:
assume that
A23: rng s1 c= (right_open_halfline x0) /\ (dom f) and
A24: ( s1 is convergent & lim s1 = x0 ) ; :: thesis:

A25: now :: thesis:

let p be Real; :: thesis:
assume 0 < p ; :: thesis:
then consider d being Real such that
A26: 0 < d and
A27: for x1 being Real st x1 in dom f & x0 < x1 & x1 < x0 + d holds
|.((f . x1) - (f . x0)).| < p by A22;
consider n being Nat such that
A28: for m being Nat st n <= m holds
|.((s1 . m) - x0).| < d by A24, A26, SEQ_2:def 7;
take k = n; :: thesis:
let m be Nat; :: thesis:
A29: m in NAT by ORDINAL1:def 12;
assume k <= m ; :: thesis:
then A30: ( s1 . m in rng s1 & |.((s1 . m) - x0).| < d ) by A28, VALUED_0:28;
A31: m in dom s1 by A29, FUNCT_2:def 1;
A32: ( rng s1 c= right_open_halfline x0 & rng s1 c= dom f ) by A23, XBOOLE_1:18;
then s1 . m in right_open_halfline x0 by VALUED_0:28;
then A33: s1 . m in ].x0,+infty.[ by LIMFUNC1:def 3;
then A34: x0 < s1 . m by XXREAL_1:235;
A35: 0 < (s1 . m) - x0 by A33, XREAL_1:50, XXREAL_1:235;
f /* s1 = f * s1 by A23, XBOOLE_1:18, FUNCT_2:def 11;
then A36: (f /* s1) . m = f . (s1 . m) by A31, FUNCT_1:13;
(s1 . m) - x0 < d by A30, A35, ABSVALUE:def 1;
then s1 . m < x0 + d by XREAL_1:19;
hence |.(((f /* s1) . m) - (f . x0)).| < p by A36, A27, A30, A32, A34; :: thesis:

end;

then f /* s1 is convergent by SEQ_2:def 6;
hence ( f /* s1 is convergent & f . x0 = lim (f /* s1) ) by A25, SEQ_2:def 7; :: thesis:

end;

hence f is_Rcontinuous_in x0 by A22, FDIFF_3:def 2; :: thesis: