:: deftheorem defines is_differentiable_on PDIFF_9:def 3 :
for Z being set
for m being non zero Nat
for f being PartFunc of (REAL m),REAL holds
( f is_differentiable_on Z iff for x being Element of REAL m st x in Z holds
f | Z is_differentiable_in x );