let m be non zero Element of NAT ; :: thesis: 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))) ) )
let i be Element of NAT ; :: thesis: 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))) ) )
let X be Subset of (REAL m); :: thesis: 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))) ) )
let f, g be PartFunc of (REAL m),REAL; :: thesis: ( X is open & 1 <= i & i <= m & f is_partial_differentiable_on X,i & g is_partial_differentiable_on X,i implies ( 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))) ) ) )
assume A1: ( X is open & 1 <= i & i <= m & f is_partial_differentiable_on X,i & g is_partial_differentiable_on X,i ) ; :: thesis: ( 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))) ) )
A2: ( X c= dom f & X c= dom g ) by A1;
A3: ( dom (f `partial| (X,i)) = X & dom (g `partial| (X,i)) = X ) by Def6, A1;
dom (f (#) g) = (dom f) /\ (dom g) by VALUED_1:def 4;
then A4: X c= dom (f (#) g) by A1, XBOOLE_1:19;

A5: now :: thesis: for x being Element of REAL m st x in X 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: ( x in X 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 x in X ; :: 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 ( f is_partial_differentiable_in x,i & g is_partial_differentiable_in x,i ) by A1, Th60;
hence ( 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))) ) by Th64; :: thesis: verum

end;

then A6: for x being Element of REAL m st x in X holds
f (#) g is_partial_differentiable_in x,i ;
then A7: f (#) g is_partial_differentiable_on X,i by A4, Th60, A1;
then A8: dom ((f (#) g) `partial| (X,i)) = X by Def6;

A9: now :: thesis: 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)))

let x be Element of REAL m; :: thesis: ( x in X implies ((f (#) g) `partial| (X,i)) /. x = ((partdiff (f,x,i)) * (g . x)) + ((f . x) * (partdiff (g,x,i))) )
assume A10: x in X ; :: thesis: ((f (#) g) `partial| (X,i)) /. x = ((partdiff (f,x,i)) * (g . x)) + ((f . x) * (partdiff (g,x,i)))
then ((f (#) g) `partial| (X,i)) /. x = partdiff ((f (#) g),x,i) by A7, Def6;
hence ((f (#) g) `partial| (X,i)) /. x = ((partdiff (f,x,i)) * (g . x)) + ((f . x) * (partdiff (g,x,i))) by A5, A10; :: thesis: verum

end;

( dom ((f `partial| (X,i)) (#) g) = (dom (f `partial| (X,i))) /\ (dom g) & dom (f (#) (g `partial| (X,i))) = (dom f) /\ (dom (g `partial| (X,i))) ) by VALUED_1:def 4;
then A11: ( dom ((f `partial| (X,i)) (#) g) = X & dom (f (#) (g `partial| (X,i))) = X ) by A3, A2, XBOOLE_1:28;
A12: dom (((f `partial| (X,i)) (#) g) + (f (#) (g `partial| (X,i)))) = (dom ((f `partial| (X,i)) (#) g)) /\ (dom (f (#) (g `partial| (X,i)))) by VALUED_1:def 1;

now :: thesis: for x being Element of REAL m st x in X holds
((f (#) g) `partial| (X,i)) . x = (((f `partial| (X,i)) (#) g) + (f (#) (g `partial| (X,i)))) . x

let x be Element of REAL m; :: thesis: ( x in X implies ((f (#) g) `partial| (X,i)) . x = (((f `partial| (X,i)) (#) g) + (f (#) (g `partial| (X,i)))) . x )
assume A13: x in X ; :: thesis: ((f (#) g) `partial| (X,i)) . x = (((f `partial| (X,i)) (#) g) + (f (#) (g `partial| (X,i)))) . x
thus ((f (#) g) `partial| (X,i)) . x = ((f (#) g) `partial| (X,i)) /. x by A13, A8, PARTFUN1:def 6
.= ((partdiff (f,x,i)) * (g . x)) + ((f . x) * (partdiff (g,x,i))) by A9, A13
.= (((f `partial| (X,i)) /. x) * (g . x)) + ((f . x) * (partdiff (g,x,i))) by A13, Def6, A1
.= (((f `partial| (X,i)) /. x) * (g . x)) + ((f . x) * ((g `partial| (X,i)) /. x)) by A13, Def6, A1
.= (((f `partial| (X,i)) . x) * (g . x)) + ((f . x) * ((g `partial| (X,i)) /. x)) by A13, A3, PARTFUN1:def 6
.= (((f `partial| (X,i)) . x) * (g . x)) + ((f . x) * ((g `partial| (X,i)) . x)) by A13, A3, PARTFUN1:def 6
.= (((f `partial| (X,i)) (#) g) . x) + ((f . x) * ((g `partial| (X,i)) . x)) by VALUED_1:5
.= (((f `partial| (X,i)) (#) g) . x) + ((f (#) (g `partial| (X,i))) . x) by VALUED_1:5
.= (((f `partial| (X,i)) (#) g) + (f (#) (g `partial| (X,i)))) . x by A13, A12, A11, VALUED_1:def 1 ; :: thesis: verum

end;

hence ( 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))) ) ) by A6, A9, A4, Th60, A1, A8, A11, A12, PARTFUN1:5; :: thesis: verum