:: deftheorem defines diff NDIFF_6:def 6 :
for S, T being RealNormSpace
for f being PartFunc of S,T
for Z being Subset of S
for i being Nat holds diff (f,i,Z) = (diff (f,Z)) . i;