let m be non zero Element of NAT ; :: thesis: 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))) )
let i be Element of NAT ; :: thesis: 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))) )
let f, g be PartFunc of (REAL m),REAL; :: thesis: 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))) )
let x be Element of REAL m; :: thesis: ( f is_partial_differentiable_in x,i & g is_partial_differentiable_in x,i implies ( 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))) ) )
assume a1: ( f is_partial_differentiable_in x,i & g is_partial_differentiable_in x,i ) ; :: thesis: ( 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))) )
set y = (proj (i,m)) . x;
dom (reproj (i,x)) = REAL by FUNCT_2:def 1;
then A2: ( (f * (reproj (i,x))) . ((proj (i,m)) . x) = f . ((reproj (i,x)) . ((proj (i,m)) . x)) & (g * (reproj (i,x))) . ((proj (i,m)) . x) = g . ((reproj (i,x)) . ((proj (i,m)) . x)) ) by FUNCT_1:13;
then A3: (f * (reproj (i,x))) . ((proj (i,m)) . x) = f . x by Th12;
(f * (reproj (i,x))) (#) (g * (reproj (i,x))) = (f (#) g) * (reproj (i,x)) by Lm5;
then (f (#) g) * (reproj (i,x)) is_differentiable_in (proj (i,m)) . x by a1, FDIFF_1:16;
hence f (#) g is_partial_differentiable_in x,i ; :: thesis: partdiff ((f (#) g),x,i) = ((partdiff (f,x,i)) * (g . x)) + ((f . x) * (partdiff (g,x,i)))
thus partdiff ((f (#) g),x,i) = diff (((f * (reproj (i,x))) (#) (g * (reproj (i,x)))),((proj (i,m)) . x)) by Lm5
.= (((g * (reproj (i,x))) . ((proj (i,m)) . x)) * (partdiff (f,x,i))) + (((f * (reproj (i,x))) . ((proj (i,m)) . x)) * (diff ((g * (reproj (i,x))),((proj (i,m)) . x)))) by a1, FDIFF_1:16
.= ((partdiff (f,x,i)) * (g . x)) + ((f . x) * (partdiff (g,x,i))) by A3, A2, Th12 ; :: thesis: verum