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