theorem Th41: :: NCFCONT1:41

for CNS1, CNS2 being ComplexNormSpace
for X being set
for f being PartFunc of CNS1,CNS2 holds
( f is_continuous_on X iff ( X c= dom f & ( for s1 being sequence of CNS1 st rng s1 c= X & s1 is convergent & lim s1 in X holds
( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) ) ) ) )