:: deftheorem Def7 defines PartDiffSeq PDIFF_9:def 7 :
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
for b₅ being Functional_Sequence of (REAL m),REAL holds
( b₅ = PartDiffSeq (f,Z,I) iff ( b₅ . 0 = f | Z & ( for i being Nat holds b₅ . (i + 1) = (b₅ . i) `partial| (Z,(I /. (i + 1))) ) ) );