:: deftheorem defines `partial| PDIFF_9:def 9 :
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 `partial| (Z,I) = (PartDiffSeq (f,Z,I)) . (len I);