theorem :: NFCONT_3:22

for X being set
for S being RealNormSpace
for f being PartFunc of REAL, the carrier of S st X c= dom f & f | X is continuous holds
( ||.f.|| | X is continuous & (- f) | X is continuous )