theorem :: NFCONT_4:18

for n being Element of NAT
for x0 being Real
for f being PartFunc of REAL,(REAL n) st x0 in dom f & f is_continuous_in x0 holds
- f is_continuous_in x0