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
diff (f,i,Z) is_differentiable_on Z ) ) )