for CNS being ComplexNormSpace
for RNS being RealNormSpace
for f1, f2 being PartFunc of CNS,RNS
for x0 being Point of CNS st f1 is_continuous_in x0 & f2 is_continuous_in x0 holds
( f1 + f2 is_continuous_in x0 & f1 - f2 is_continuous_in x0 )