:: deftheorem defines is_continuous_on PDIFF_9:def 2 :
for m being non zero Element of NAT
for Z being set
for f being PartFunc of (REAL m),REAL holds
( f is_continuous_on Z iff for x0 being Element of REAL m st x0 in Z holds
f | Z is_continuous_in x0 );