let S, T be RealNormSpace; :: thesis:
let f be PartFunc of S,T; :: thesis:
let x0 be Point of S; :: 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 Point of S 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 N1 be Neighbourhood of f /. x0; :: thesis:
consider r being Real such that
A2: 0 < r and
A3: { y where y is Point of T : ||.(y - (f /. x0)).|| < r } c= N1 by Def1;
consider s being Real such that
A4: 0 < s and
A5: for x1 being Point of S st x1 in dom f & ||.(x1 - x0).|| < s holds
||.((f /. x1) - (f /. x0)).|| < r by A1, A2, Th7;
reconsider s = s as Real ;
reconsider N = { z where z is Point of S : ||.(z - x0).|| < s } as Neighbourhood of x0 by A4, Th3;
take N ; :: thesis:
let x1 be Point of S; :: thesis:
assume that
A6: x1 in dom f and
A7: x1 in N ; :: thesis:
ex z being Point of S st
( x1 = z & ||.(z - x0).|| < s ) by A7;
then ||.((f /. x1) - (f /. x0)).|| < r by A5, A6;
then f /. x1 in { y where y is Point of T : ||.(y - (f /. x0)).|| < r } ;
hence f /. x1 in N1 by A3; :: thesis:

end;

assume that
A8: x0 in dom f and
A9: for N1 being Neighbourhood of f /. x0 ex N being Neighbourhood of x0 st
for x1 being Point of S st x1 in dom f & x1 in N holds
f /. x1 in N1 ; :: thesis:

let r be Real; :: thesis:
assume A10: 0 < r ; :: thesis:
reconsider rr = r as Real ;
reconsider N1 = { y where y is Point of T : ||.(y - (f /. x0)).|| < rr } as Neighbourhood of f /. x0 by Th3, A10;
consider N2 being Neighbourhood of x0 such that
A11: for x1 being Point of S st x1 in dom f & x1 in N2 holds
f /. x1 in N1 by A9;
consider s being Real such that
A12: 0 < s and
A13: { z where z is Point of S : ||.(z - x0).|| < s } c= N2 by Def1;
take s = s; :: thesis:
for x1 being Point of S st x1 in dom f & ||.(x1 - x0).|| < s holds
||.((f /. x1) - (f /. x0)).|| < r

let x1 be Point of S; :: thesis:
assume that
A14: x1 in dom f and
A15: ||.(x1 - x0).|| < s ; :: thesis:
x1 in { z where z is Point of S : ||.(z - x0).|| < s } by A15;
then f /. x1 in N1 by A11, A13, A14;
then ex y being Point of T st
( f /. x1 = y & ||.(y - (f /. x0)).|| < r ) ;
hence ||.((f /. x1) - (f /. x0)).|| < r ; :: thesis:

end;

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

end;