for m being non zero Element of NAT
for Z being set
for f being PartFunc of (REAL m),REAL
for g being PartFunc of (REAL m),(REAL 1) st <>* f = g holds
( ( Z c= dom f & f is_differentiable_on Z ) iff g is_differentiable_on Z )