:: deftheorem Def6 defines PartDiffSeq NDIFF14:def 6 :
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 b₆ being FinSequence holds
( b₆ = PartDiffSeq (f,Z,I) iff ( dom b₆ = dom I & b₆ . 1 = f `partial| (Z,(I . 1)) & ( for i being Nat st 1 <= i & i < len I holds
ex g being PartFunc of (product S),(Partdiff_SP (S,T,I,i)) st
( b<sub>6</sub> . i = g & b<sub>6</sub> . (i + 1) = g `partial| (Z,(I . (i + 1))) ) ) ) );