let x0 be Real; :: thesis:
let S be RealNormSpace; :: thesis:
let f be PartFunc of REAL, the carrier of S; :: thesis:
thus ( f is_continuous_in x0 implies ( x0 in dom f & ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Real st x1 in dom f & |.(x1 - x0).| < s holds
||.((f /. x1) - (f /. x0)).|| < r ) ) ) ) ) :: thesis:

proof

assume A1: f is_continuous_in x0 ; :: thesis:
hence x0 in dom f ; :: thesis:
given r being Real such that A2: 0 < r and
A3: for s being Real holds
( not 0 < s or ex x1 being Real st
( x1 in dom f & |.(x1 - x0).| < s & not ||.((f /. x1) - (f /. x0)).|| < r ) ) ; :: thesis:
defpred S₁[ Nat, Real] means ( $2 in dom f & |.($2 - x0).| < 1 / ($1 + 1) & not ||.((f /. $2) - (f /. x0)).|| < r );
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:
0 < (n + 1) " ;
then 0 < 1 / (n + 1) by XCMPLX_1:215;
then consider x1 being Real such that
A5: ( x1 in dom f & |.(x1 - x0).| < 1 / (n + 1) & not ||.((f /. x1) - (f /. x0)).|| < r ) by A3;
take x1 ; :: thesis:
thus ( x1 is set & x1 is Element of REAL & S₁[n,x1] ) by A5; :: thesis:

end;

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

now :: thesis:

let x be object ; :: thesis:
assume x in rng s1 ; :: thesis:
then ex n being Element of NAT st x = s1 . n by FUNCT_2:113;
hence x in dom f by A6; :: thesis:

end;

then A7: rng s1 c= dom f by TARSKI:def 3;

A8: now :: thesis:

let s be Real; :: thesis:
assume A9: 0 < s ; :: thesis:
consider n being Nat such that
A10: s " < n by SEQ_4:3;
(s ") + 0 < n + 1 by A10, XREAL_1:8;
then 1 / (n + 1) < 1 / (s ") by A9, XREAL_1:76;
then A11: 1 / (n + 1) < s by XCMPLX_1:216;
take k = n; :: thesis:
let m be Nat; :: thesis:
A12: 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 1 / (m + 1) < s by A11, XXREAL_0:2;
hence |.((s1 . m) - x0).| < s by A6, XXREAL_0:2, A12; :: thesis:

end;

then A13: 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, A7, A13;
then consider n being Nat such that
A14: for m being Nat st n <= m holds
||.(((f /* s1) . m) - (f /. x0)).|| < r by A2, NORMSP_1:def 7;
A15: n in NAT by ORDINAL1:def 12;
||.(((f /* s1) . n) - (f /. x0)).|| < r by A14;
then ||.((f /. (s1 . n)) - (f /. x0)).|| < r by A7, FUNCT_2:109, A15;
hence contradiction by A6, A15; :: thesis:

end;

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

now :: thesis:

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

A19: now :: thesis:

let p be Real; :: thesis:
assume 0 < p ; :: thesis:
then consider s being Real such that
A20: 0 < s and
A21: for x1 being Real st x1 in dom f & |.(x1 - x0).| < s holds
||.((f /. x1) - (f /. x0)).|| < p by A16;
consider n being Nat such that
A22: for m being Nat st n <= m holds
|.((s1 . m) - x0).| < s by A18, A20, SEQ_2:def 7;
take k = n; :: thesis:
let m be Nat; :: thesis:
A23: m in NAT by ORDINAL1:def 12;
assume k <= m ; :: thesis:
then ( s1 . m in rng s1 & |.((s1 . m) - x0).| < s ) by A22, VALUED_0:28;
then ||.((f /. (s1 . m)) - (f /. x0)).|| < p by A17, A21;
hence ||.(((f /* s1) . m) - (f /. x0)).|| < p by A17, FUNCT_2:109, A23; :: thesis:

end;

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

end;

hence f is_continuous_in x0 by A16; :: thesis: