let x0 be real number ; :: thesis:
let f be PartFunc of REAL ,REAL ; :: thesis:
thus ( f is_continuous_in x0 implies for r being real number st 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r ) ) ) :: thesis:

assume A1: f is_continuous_in x0 ; :: thesis:
given r being real number such that A2: ( 0 < r & ( for s being real number holds
( not 0 < s or ex x1 being real number st
( x1 in dom f & abs (x1 - x0) < s & not abs ((f . x1) - (f . x0)) < r ) ) ) ) ; :: thesis:
defpred S₁[ Element of NAT , real number ] means ( $2 in dom f & abs ($2 - x0) < 1 / ($1 + 1) & not abs ((f . $2) - (f . x0)) < r );
A3: for n being Element of NAT ex p being Real st S₁[n,p]

let n be Element of NAT ; :: thesis:
0 < (n + 1) " ;
then 0 < 1 / (n + 1) by XCMPLX_1:217;
then consider p being real number such that
A4: ( p in dom f & abs (p - x0) < 1 / (n + 1) & not abs ((f . p) - (f . x0)) < r ) by A2;
take p ; :: thesis:
thus ( p is Real & S₁[n,p] ) by A4; :: 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(A3);
A6: rng s1 c= dom f

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in rng s1 ; :: thesis:
then ex n being Element of NAT st x = s1 . n by FUNCT_2:190;
hence x in dom f by A5; :: thesis:

end;

A7: now

let n be Element of NAT ; :: thesis:
not abs ((f . (s1 . n)) - (f . x0)) < r by A5;
hence not abs (((f /* s1) . n) - (f . x0)) < r by A6, FUNCT_2:185; :: thesis:

end;

A8: now

let s be real number ; :: thesis:
assume 0 < s ; :: thesis:
then A9: 0 < s " ;
consider n being Element of NAT such that
A10: s " < n by SEQ_4:10;
take k = n; :: thesis:
let m be Element of NAT ; :: thesis:
assume A11: k <= m ; :: thesis:
(s " ) + 0 < n + 1 by A10, XREAL_1:10;
then 1 / (n + 1) < 1 / (s " ) by A9, XREAL_1:78;
then A12: 1 / (n + 1) < s by XCMPLX_1:218;
k + 1 <= m + 1 by A11, XREAL_1:8;
then 1 / (m + 1) <= 1 / (k + 1) by XREAL_1:120;
then 1 / (m + 1) < s by A12, XXREAL_0:2;
hence abs ((s1 . m) - x0) < s by A5, XXREAL_0:2; :: thesis:

end;

then A14: s1 is convergent by SEQ_2:def 6;
then lim s1 = x0 by A8, SEQ_2:def 7;
then ( f /* s1 is convergent & f . x0 = lim (f /* s1) ) by A1, A6, A14, Def1;
then consider n being Element of NAT such that
A15: for m being Element of NAT st n <= m holds
abs (((f /* s1) . m) - (f . x0)) < r by A2, SEQ_2:def 7;
abs (((f /* s1) . n) - (f . x0)) < r by A15;
hence contradiction by A7; :: thesis:

end;

assume A16: for r being real number st 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r ) ) ; :: thesis:

let s1 be Real_Sequence; :: thesis:
assume A17: ( rng s1 c= dom f & s1 is convergent & lim s1 = x0 ) ; :: thesis:

A18: now

let p be real number ; :: thesis:
assume 0 < p ; :: thesis:
then consider s being real number such that
A19: ( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < p ) ) by A16;
consider n being Element of NAT such that
A20: for m being Element of NAT st n <= m holds
abs ((s1 . m) - x0) < s by A17, A19, SEQ_2:def 7;
take k = n; :: thesis:
let m be Element of NAT ; :: thesis:
assume A21: k <= m ; :: thesis:
A22: s1 . m in rng s1 by VALUED_0:28;
abs ((s1 . m) - x0) < s by A20, A21;
then abs ((f . (s1 . m)) - (f . x0)) < p by A17, A19, A22;
hence abs (((f /* s1) . m) - (f . x0)) < p by A17, FUNCT_2:185; :: thesis:

end;

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

end;

hence f is_continuous_in x0 by Def1; :: thesis: