for S being RealNormSpace
for f being PartFunc of REAL, the carrier of S
for x0 being Real holds
( f is_continuous_in x0 iff ( x0 in dom f & ( for N1 being Neighbourhood of f /. x0 ex N being Neighbourhood of x0 st f .: N c= N1 ) ) )