:: deftheorem Def5 defines differentiable NDIFF_4:def 5 :
for n being non zero Element of NAT
for f being PartFunc of REAL,(REAL n) holds
( f is differentiable iff f is_differentiable_on dom f );