theorem Th21: :: HFDIFF_1:21

for r being Real
for n being Element of NAT
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st f is_differentiable_on n,Z holds
(diff ((r (#) f),Z)) . n = r (#) ((diff (f,Z)) . n)