theorem Th24: :: NDIFF11:24

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 being Element of REAL m
for a being Real holds (diff (f,x)) . (a * u) = a * ((diff (f,x)) . u)