theorem Th64: :: PDIFF_9:64

for m being non zero Element of NAT
for i being Element of NAT
for f, g being PartFunc of (REAL m),REAL
for x being Element of REAL m st f is_partial_differentiable_in x,i & g is_partial_differentiable_in x,i holds
( f (#) g is_partial_differentiable_in x,i & partdiff ((f (#) g),x,i) = ((partdiff (f,x,i)) * (g . x)) + ((f . x) * (partdiff (g,x,i))) )