:: deftheorem defines is_partial_differentiable_up_to_order PDIFF_9:def 11 :
for m being non zero Element of NAT
for f being PartFunc of (REAL m),REAL
for k being Nat
for Z being set holds
( f is_partial_differentiable_up_to_order k,Z iff for I being non empty FinSequence of NAT st len I <= k & rng I c= Seg m holds
f is_partial_differentiable_on Z,I );