theorem Th23: :: NDIFF11:23

for m being non zero Nat
for f being PartFunc of (REAL m),REAL
for x being Element of REAL m st f is_differentiable_in x holds
for u, v being Element of REAL m holds (diff (f,x)) . (u + v) = ((diff (f,x)) . u) + ((diff (f,x)) . v)