theorem Th6: :: HFDIFF_1:6

for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st f | Z is_differentiable_on Z holds
f is_differentiable_on Z