:: deftheorem defines diff_SP NDIFF_6:def 3 :
for S, T being RealNormSpace
for i being Nat holds diff_SP (i,S,T) = (diff_SP (S,T)) . i;