theorem :: NCFCONT1:65

for CNS1, CNS2 being ComplexNormSpace
for X, X1 being set
for f1, f2 being PartFunc of CNS1,CNS2 st f1 is_continuous_on X & f2 is_continuous_on X1 holds
( f1 + f2 is_continuous_on X /\ X1 & f1 - f2 is_continuous_on X /\ X1 )