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 + 1),Z) = (diff (f,i,Z)) `| Z