:: deftheorem defines is_partial_differentiable_on NDIFF14:def 8 :
for S being RealNormSpace-Sequence
for T being RealNormSpace
for Z being Subset of (product S)
for I being non empty FinSequence of dom S
for f being PartFunc of (product S),T holds
( f is_partial_differentiable_on Z,I iff ( f is_partial_differentiable_on Z,I . 1 & ( for i being Nat st 1 <= i & i < len I holds
PartDiffSeq (f,Z,I,i) is_partial_differentiable_on Z,I . (i + 1) ) ) );