theorem :: NDIFF_4:22

for n being non zero Element of NAT
for Z being open Subset of REAL
for f being differentiable PartFunc of REAL,(REAL n) st Z c= dom f holds
f is_differentiable_on Z by Def5, Th21;