theorem Th14: :: NCFCONT1:14

for CNS1, CNS2 being ComplexNormSpace
for f being PartFunc of CNS1,CNS2
for x0 being Point of CNS1 holds
( f is_continuous_in x0 iff ( x0 in dom f & ( for N1 being Neighbourhood of f /. x0 ex N being Neighbourhood of x0 st
for x1 being Point of CNS1 st x1 in dom f & x1 in N holds
f /. x1 in N1 ) ) )