theorem Th10: :: NDIFF_3:10

for F being RealNormSpace
for Z being open Subset of REAL
for f being PartFunc of REAL, the carrier of F 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 ) ) )