:: deftheorem defines is_continuous_on DUALSP04:def 6 :
for X being RealUnitarySpace
for f being PartFunc of the carrier of X,REAL
for Y being set holds
( f is_continuous_on Y iff ( Y c= dom f & ( for x0 being Point of X st x0 in Y holds
f | Y is_continuous_in x0 ) ) );