theorem Th5: :: NDIFF_4:5

for n being non zero Element of NAT
for Z being open Subset of REAL
for f being PartFunc of REAL,(REAL n) holds
( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Real st x in Z holds
f is_differentiable_in x ) ) )