:: deftheorem Def7 defines PartDiffSeq NDIFF14:def 7 :
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
for i being Nat st 1 <= i & i <= len I holds
PartDiffSeq (f,Z,I,i) = (PartDiffSeq (f,Z,I)) . i;