theorem Th9: :: NDIFF_3:9

for F being RealNormSpace
for X being set
for f being PartFunc of REAL, the carrier of F st f is_differentiable_on X holds
X is Subset of REAL by XBOOLE_1:1;