:: deftheorem defines is_continuous_on NCFCONT1:def 13 :
for RNS being RealNormSpace
for CNS being ComplexNormSpace
for g being PartFunc of RNS,CNS
for X being set holds
( g is_continuous_on X iff ( X c= dom g & ( for x0 being Point of RNS st x0 in X holds
g | X is_continuous_in x0 ) ) );