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