theorem :: NCFCONT1:40

for CNS being ComplexNormSpace
for RNS being RealNormSpace
for f being PartFunc of RNS,CNS
for x0 being Point of RNS st f is_continuous_in x0 holds
( ||.f.|| is_continuous_in x0 & - f is_continuous_in x0 )