for m, n being non zero Nat
for f being PartFunc of (REAL m),(REAL n)
for Z being Subset of (REAL m) st ex Z0 being Subset of (REAL-NS m) st
( Z = Z0 & Z0 is open ) holds
( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Element of REAL m st x in Z holds
f is_differentiable_in x ) ) )