theorem Th22: :: NDIFF_6:22

for S, T being RealNormSpace
for Z being Subset of S
for n being Nat
for f, g being PartFunc of S,T st 1 <= n & f is_differentiable_on n,Z & g is_differentiable_on n,Z holds
for i being Nat st i <= n holds
diff ((f - g),i,Z) = (diff (f,i,Z)) - (diff (g,i,Z))