theorem Th43: :: NCFCONT1:43

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