theorem Th27: :: NDIFF14:27

for S being RealNormSpace-Sequence
for T being RealNormSpace
for Z being Subset of (product S)
for f being PartFunc of (product S),T
for a being Real
for i being set st Z is open & i in dom S & f is_partial_differentiable_on Z,i holds
( a (#) f is_partial_differentiable_on Z,i & (a (#) f) `partial| (Z,i) = a (#) (f `partial| (Z,i)) )