for CNS1, CNS2 being ComplexNormSpace
for f being PartFunc of CNS1,CNS2
for x0 being Point of CNS1 st f is_continuous_in x0 holds
( ||.f.|| is_continuous_in x0 & - f is_continuous_in x0 )