:: deftheorem defines is_partial_differentiable_on PDIFF_9:def 8 :
for m being non zero Element of NAT
for Z being set
for I being FinSequence of NAT
for f being PartFunc of (REAL m),REAL holds
( f is_partial_differentiable_on Z,I iff for i being Element of NAT st i <= (len I) - 1 holds
(PartDiffSeq (f,Z,I)) . i is_partial_differentiable_on Z,I /. (i + 1) );