:: deftheorem defines is_differentiable_on NDIFF_4:def 3 :
for n being non zero Element of NAT
for f being PartFunc of REAL,(REAL n)
for X being set holds
( f is_differentiable_on X iff ( X c= dom f & ( for x being Real st x in X holds
f | X is_differentiable_in x ) ) );