theorem :: NFCONT_1:24

for S, T being RealNormSpace
for f being PartFunc of S,T
for x0 being Point of S st x0 in dom f holds
f is_continuous_on {x0}