theorem :: NDIFF_3:26

for F being RealNormSpace
for Z being open Subset of REAL
for f being differentiable PartFunc of REAL, the carrier of F st Z c= dom f holds
f is_differentiable_on Z by Def7, Th24;