:: deftheorem defines is_differentiable_on NDIFF_6:def 7 :
for S, T being RealNormSpace
for f being PartFunc of S,T
for Z being Subset of S
for n being Nat holds
( f is_differentiable_on n,Z iff ( Z c= dom f & ( for i being Nat st i <= n - 1 holds
modetrans (((diff (f,Z)) . i),S,(diff_SP (i,S,T))) is_differentiable_on Z ) ) );