:: deftheorem defines is_differentiable_on NDIFF_3:def 5 :
for F being RealNormSpace
for f being PartFunc of REAL, the carrier of F
for X being set holds
( f is_differentiable_on X iff ( X c= dom f & ( for x being Real st x in X holds
f | X is_differentiable_in x ) ) );