theorem :: NCFCONT1:74

for CNS1, CNS2 being ComplexNormSpace
for f being PartFunc of CNS1,CNS2 st f is total & ( for x1, x2 being Point of CNS1 holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ) & ex x0 being Point of CNS1 st f is_continuous_in x0 holds
f is_continuous_on the carrier of CNS1