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 f .: N c= 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 N being Neighbourhood of x0 such that
A2: for x1 being Point of S st x1 in dom f & x1 in N holds
f /. x1 in N1 by A1, Th9;
take N ; :: thesis:

let r be object ; :: thesis:
assume r in f .: N ; :: thesis:
then consider x being Point of S such that
A3: x in dom f and
A4: x in N and
A5: r = f . x by PARTFUN2:59;
r = f /. x by A3, A5, PARTFUN1:def 6;
hence r in N1 by A2, A3, A4; :: thesis:

end;

hence f .: N c= N1 ; :: thesis:

end;

let N1 be Neighbourhood of f /. x0; :: thesis:
consider N being Neighbourhood of x0 such that
A8: f .: N c= N1 by A7;
take N = N; :: thesis:
let x1 be Point of S; :: thesis:
assume that
A9: x1 in dom f and
A10: x1 in N ; :: thesis:
f . x1 in f .: N by A9, A10, FUNCT_1:def 6;
then f . x1 in N1 by A8;
hence f /. x1 in N1 by A9, PARTFUN1:def 6; :: thesis:

end;