:: deftheorem defines PartdiffSP NDIFF14:def 5 :
for S being RealNormSpace-Sequence
for T being RealNormSpace
for I being non empty FinSequence of dom S holds PartdiffSP (S,T,I) = (Partdiff_SP (S,T,I)) . (len I);