let S be RealNormSpace; :: thesis:
let f be PartFunc of REAL, the carrier of S; :: thesis:
let x0 be Real; :: thesis:
thus ( f is_continuous_in x0 implies ( x0 in dom f & ( for N1 being Neighbourhood of f /. x0 ex N being Neighbourhood of x0 st
for x1 being Real st x1 in dom f & x1 in N holds
f /. x1 in N1 ) ) ) :: thesis:

assume A1: f is_continuous_in x0 ; :: thesis:
hence x0 in dom f ; :: thesis:
let N01 be Neighbourhood of f /. x0; :: thesis:
consider r being Real such that
A2: 0 < r and
A3: { p where p is Point of S : ||.(p - (f /. x0)).|| < r } c= N01 by NFCONT_1:def 1;
set N1 = { p where p is Point of S : ||.(p - (f /. x0)).|| < r } ;
consider s being Real such that
A4: 0 < s and
A5: for x1 being Real st x1 in dom f & |.(x1 - x0).| < s holds
||.((f /. x1) - (f /. x0)).|| < r by A1, A2, Th8;
reconsider N = ].(x0 - s),(x0 + s).[ as Neighbourhood of x0 by A4, RCOMP_1:def 6;
take N ; :: thesis:
let x1 be Real; :: thesis:
assume that
A6: x1 in dom f and
A7: x1 in N ; :: thesis:
|.(x1 - x0).| < s by A7, RCOMP_1:1;
then ||.((f /. x1) - (f /. x0)).|| < r by A5, A6;
then f /. x1 in { p where p is Point of S : ||.(p - (f /. x0)).|| < r } ;
hence f /. x1 in N01 by A3; :: thesis:

end;

assume A8: ( x0 in dom f & ( for N1 being Neighbourhood of f /. x0 ex N being Neighbourhood of x0 st
for x1 being Real st x1 in dom f & x1 in N holds
f /. x1 in N1 ) ) ; :: thesis:

let r be Real; :: thesis:
assume 0 < r ; :: thesis:
then reconsider N1 = { p where p is Point of S : ||.(p - (f /. x0)).|| < r } as Neighbourhood of f /. x0 by NFCONT_1:3;
consider N2 being Neighbourhood of x0 such that
A9: for x1 being Real st x1 in dom f & x1 in N2 holds
f /. x1 in N1 by A8;
consider s being Real such that
A10: 0 < s and
A11: N2 = ].(x0 - s),(x0 + s).[ by RCOMP_1:def 6;
take s = s; :: thesis:
for x1 being Real st x1 in dom f & |.(x1 - x0).| < s holds
||.((f /. x1) - (f /. x0)).|| < r

let x1 be Real; :: thesis:
assume that
A12: x1 in dom f and
A13: |.(x1 - x0).| < s ; :: thesis:
x1 in N2 by A11, A13, RCOMP_1:1;
then f /. x1 in N1 by A9, A12;
then ex p being Point of S st
( p = f /. x1 & ||.(p - (f /. x0)).|| < r ) ;
hence ||.((f /. x1) - (f /. x0)).|| < r ; :: thesis:

end;

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

end;