theorem Th25: :: NDIFF_6:25

for S, T being RealNormSpace
for Z being Subset of S
for n being Nat
for r being Real
for f being PartFunc of S,T st 1 <= n & f is_differentiable_on n,Z holds
r (#) f is_differentiable_on n,Z