theorem :: NDIFF_3:11

for F being RealNormSpace
for Y being Subset of REAL
for f being PartFunc of REAL, the carrier of F st f is_differentiable_on Y holds
Y is open