for m being non zero Element of NAT
for i being Element of NAT
for X being Subset of (REAL m)
for f, g being PartFunc of (REAL m),REAL st X is open & 1 <= i & i <= m & f is_partial_differentiable_on X,i & g is_partial_differentiable_on X,i holds
( f (#) g is_partial_differentiable_on X,i & (f (#) g) `partial| (X,i) = ((f `partial| (X,i)) (#) g) + (f (#) (g `partial| (X,i))) & ( for x being Element of REAL m st x in X holds
((f (#) g) `partial| (X,i)) /. x = ((partdiff (f,x,i)) * (g . x)) + ((f . x) * (partdiff (g,x,i))) ) )