theorem :: FDIFF_1:28

for Z being open Subset of REAL
for f being differentiable PartFunc of REAL,REAL st Z c= dom f holds
f is_differentiable_on Z by Th26, Def8;