theorem Th6: :: NFCONT_3:6

for X being set
for x0 being Real
for S being RealNormSpace
for f being PartFunc of REAL, the carrier of S st x0 in X & f is_continuous_in x0 holds
f | X is_continuous_in x0