theorem :: NDIFF_3:19

for F being RealNormSpace
for r being Real
for Z being open Subset of REAL
for f being PartFunc of REAL, the carrier of F st Z c= dom (r (#) 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)) ) )