let m be non empty 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 ( 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))) )
then P1: ( f * (reproj (i,x)) is_differentiable_in (proj (i,m)) . x & g * (reproj (i,x)) is_differentiable_in (proj (i,m)) . x ) by PDIFF_1:def 11;
set y = (proj (i,m)) . x;
dom (reproj (i,x)) = REAL by FUNCT_2:def 1;
then P7: ( (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 P6: (f * (reproj (i,x))) . ((proj (i,m)) . x) = f . x by LMMMTh6;
(f * (reproj (i,x))) (#) (g * (reproj (i,x))) = (f (#) g) * (reproj (i,x)) by LM1291;
then (f (#) g) * (reproj (i,x)) is_differentiable_in (proj (i,m)) . x by P1, FDIFF_1:16;
hence f (#) g is_partial_differentiable_in x,i by PDIFF_1:def 11; :: 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 LM1291
.= (((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 P1, FDIFF_1:16
.= ((partdiff (f,x,i)) * (g . x)) + ((f . x) * (partdiff (g,x,i))) by P6, P7, LMMMTh6 ; :: thesis: verum