theorem Th13: :: NDIFF_4:13

for r being Real
for n being non zero Element of NAT
for Z being open Subset of REAL
for f being PartFunc of REAL,(REAL n) st Z c= dom f & f is_differentiable_on Z holds
( r (#) f is_differentiable_on Z & ( for x being Real st x in Z holds
((r (#) f) `| Z) . x = r * (diff (f,x)) ) )