let m be non zero Element of NAT ; :: thesis: for X being Subset of (REAL m) st X is open holds
for i being Element of NAT
for f, g being PartFunc of (REAL m),REAL st f is_partial_differentiable_up_to_order i,X & g is_partial_differentiable_up_to_order i,X holds
f (#) g is_partial_differentiable_up_to_order i,X
let Z be Subset of (REAL m); :: thesis: ( Z is open implies for i being Element of NAT
for f, g being PartFunc of (REAL m),REAL st f is_partial_differentiable_up_to_order i,Z & g is_partial_differentiable_up_to_order i,Z holds
f (#) g is_partial_differentiable_up_to_order i,Z )
assume A1: Z is open ; :: thesis: for i being Element of NAT
for f, g being PartFunc of (REAL m),REAL st f is_partial_differentiable_up_to_order i,Z & g is_partial_differentiable_up_to_order i,Z holds
f (#) g is_partial_differentiable_up_to_order i,Z
defpred S₁[ Nat] means for f, g being PartFunc of (REAL m),REAL st f is_partial_differentiable_up_to_order $1,Z & g is_partial_differentiable_up_to_order $1,Z holds
f (#) g is_partial_differentiable_up_to_order $1,Z;
A2: S₁[ 0 ]

proof

let f, g be PartFunc of (REAL m),REAL; :: thesis: ( f is_partial_differentiable_up_to_order 0 ,Z & g is_partial_differentiable_up_to_order 0 ,Z implies f (#) g is_partial_differentiable_up_to_order 0 ,Z )
thus ( f is_partial_differentiable_up_to_order 0 ,Z & g is_partial_differentiable_up_to_order 0 ,Z implies f (#) g is_partial_differentiable_up_to_order 0 ,Z ) ; :: thesis: verum

end;

A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]
let f, g be PartFunc of (REAL m),REAL; :: thesis: ( f is_partial_differentiable_up_to_order k + 1,Z & g is_partial_differentiable_up_to_order k + 1,Z implies f (#) g is_partial_differentiable_up_to_order k + 1,Z )
assume A5: ( f is_partial_differentiable_up_to_order k + 1,Z & g is_partial_differentiable_up_to_order k + 1,Z ) ; :: thesis: f (#) g is_partial_differentiable_up_to_order k + 1,Z
then A6: ( f is_partial_differentiable_up_to_order k,Z & g is_partial_differentiable_up_to_order k,Z ) by Th84, NAT_1:11;

now :: thesis: for I being non empty FinSequence of NAT st len I <= k + 1 & rng I c= Seg m holds
f (#) g is_partial_differentiable_on Z,I

let I be non empty FinSequence of NAT ; :: thesis: ( len I <= k + 1 & rng I c= Seg m implies f (#) g is_partial_differentiable_on Z,b₁ )
assume A7: ( len I <= k + 1 & rng I c= Seg m ) ; :: thesis: f (#) g is_partial_differentiable_on Z,b₁
then A8: ( f is_partial_differentiable_on Z,I & g is_partial_differentiable_on Z,I ) by A5;
A9: 1 <= len I by FINSEQ_1:20;
then A10: 1 in dom I by FINSEQ_3:25;
then A11: I /. 1 = I . 1 by PARTFUN1:def 6;
A12: I . 1 in rng I by A10, FUNCT_1:3;
then I . 1 in Seg m by A7;
then reconsider i = I . 1 as Element of NAT ;
A13: ( 1 <= i & i <= m ) by A12, A7, FINSEQ_1:1;

per cases ( 1 = len I or 1 <> len I ) ;

suppose 1 = len I ; :: thesis: f (#) g is_partial_differentiable_on Z,b₁

then A14: I = <*(I . 1)*> by FINSEQ_5:14;
then ( f is_partial_differentiable_on Z,i & g is_partial_differentiable_on Z,i ) by A8;
then f (#) g is_partial_differentiable_on Z,i by A13, Th68, A1;
hence f (#) g is_partial_differentiable_on Z,I by A14; :: thesis: verum

end;

suppose 1 <> len I ; :: thesis: f (#) g is_partial_differentiable_on Z,b₁

then 1 < len I by A9, XXREAL_0:1;
then 1 + 1 <= len I by NAT_1:13;
then 1 <= (len I) - 1 by XREAL_1:19;
then 1 <= len (I /^ 1) by A9, RFINSEQ:def 1;
then reconsider J = I /^ 1 as non empty FinSequence of NAT ;
set I1 = <*i*>;
(len I) - 1 <= k by A7, XREAL_1:20;
then A15: len J <= k by A9, RFINSEQ:def 1;
A16: I = <*(I /. 1)*> ^ (I /^ 1) by FINSEQ_5:29;
then A17: ( rng <*i*> c= rng I & rng J c= rng I ) by A11, FINSEQ_1:29, FINSEQ_1:30;
then A18: rng J c= Seg m by A7;
I = <*i*> ^ J by A11, FINSEQ_5:29;
then A19: ( f is_partial_differentiable_on Z,i & g is_partial_differentiable_on Z,i ) by A8, Th80;
then A20: f (#) g is_partial_differentiable_on Z,i by A13, Th68, A1;
then A21: f (#) g is_partial_differentiable_on Z,<*i*> ;
A22: (f (#) g) `partial| (Z,<*i*>) = (f (#) g) `partial| (Z,i) by A1, A13, Th82, A20
.= ((f `partial| (Z,i)) (#) g) + (f (#) (g `partial| (Z,i))) by A19, A13, Th68, A1
.= ((f `partial| (Z,<*i*>)) (#) g) + (f (#) (g `partial| (Z,i))) by A1, A13, Th82, A19
.= ((f `partial| (Z,<*i*>)) (#) g) + (f (#) (g `partial| (Z,<*i*>))) by A1, A13, Th82, A19 ;
( len <*i*> = 1 & rng <*i*> c= Seg m ) by A17, A7, FINSEQ_1:39;
then ( f `partial| (Z,<*i*>) is_partial_differentiable_up_to_order k,Z & g `partial| (Z,<*i*>) is_partial_differentiable_up_to_order k,Z ) by Th83, A5;
then ( (f `partial| (Z,<*i*>)) (#) g is_partial_differentiable_up_to_order k,Z & f (#) (g `partial| (Z,<*i*>)) is_partial_differentiable_up_to_order k,Z ) by A4, A6;
then ( (f `partial| (Z,<*i*>)) (#) g is_partial_differentiable_on Z,J & f (#) (g `partial| (Z,<*i*>)) is_partial_differentiable_on Z,J ) by A15, A18;
then ((f `partial| (Z,<*i*>)) (#) g) + (f (#) (g `partial| (Z,<*i*>))) is_partial_differentiable_on Z,J by A1, A18, Th75;
hence f (#) g is_partial_differentiable_on Z,I by A21, A16, A11, A22, Th80; :: thesis: verum

end;

end;

end;

hence f (#) g is_partial_differentiable_up_to_order k + 1,Z ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A3);
hence for i being Element of NAT
for f, g being PartFunc of (REAL m),REAL st f is_partial_differentiable_up_to_order i,Z & g is_partial_differentiable_up_to_order i,Z holds
f (#) g is_partial_differentiable_up_to_order i,Z ; :: thesis: verum