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 f .: N c= N1 ) ) ) :: thesis:

proof

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 Real st x1 in dom f & x1 in N holds
f /. x1 in N1 by A1, Th9;
take N ; :: thesis:

now :: thesis:

let r be object ; :: thesis:
assume r in f .: N ; :: thesis:
then consider x being Element of REAL such that
A3: ( x in dom f & x in N & r = f . x ) by PARTFUN2:59;
r = f /. x by A3, PARTFUN1:def 6;
hence r in N1 by A2, A3; :: thesis:

end;

hence f .: N c= N1 by TARSKI:def 3; :: thesis:

end;

assume A4: ( x0 in dom f & ( for N1 being Neighbourhood of f /. x0 ex N being Neighbourhood of x0 st f .: N c= N1 ) ) ; :: thesis:

now :: thesis:

let N1 be Neighbourhood of f /. x0; :: thesis:
consider N being Neighbourhood of x0 such that
A5: f .: N c= N1 by A4;
take N = N; :: thesis:
let x1 be Real; :: thesis:
assume A6: ( x1 in dom f & x1 in N ) ; :: thesis:
then f . x1 in f .: N by FUNCT_1:def 6;
then f /. x1 in f .: N by A6, PARTFUN1:def 6;
hence f /. x1 in N1 by A5; :: thesis:

end;

hence f is_continuous_in x0 by A4, Th9; :: thesis: