:: deftheorem Def7 defines differentiable NDIFF_3:def 7 :
for F being RealNormSpace
for f being PartFunc of REAL, the carrier of F holds
( f is differentiable iff f is_differentiable_on dom f );