theorem :: NFCONT_4:13

for n being Element of NAT
for x0 being Real
for f being PartFunc of REAL,(REAL n) st ex N being Neighbourhood of x0 st (dom f) /\ N = {x0} holds
f is_continuous_in x0