let m be non empty 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 AS: 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₁[ Element of 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;
P9: 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 )
assume ( f is_partial_differentiable_up_to_order 0 ,Z & g is_partial_differentiable_up_to_order 0 ,Z ) ; :: thesis: f (#) g is_partial_differentiable_up_to_order 0 ,Z
for I being non empty FinSequence of NAT st len I <= 0 & rng I c= Seg m holds
f (#) g is_partial_differentiable_on Z,I by FINSEQ_1:20;
hence f (#) g is_partial_differentiable_up_to_order 0 ,Z by TDef9; :: thesis: verum

end;

P7: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume P71: 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 R71: ( 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 R711: ( f is_partial_differentiable_up_to_order k,Z & g is_partial_differentiable_up_to_order k,Z ) by XCW0410, 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 P72: ( len I <= k + 1 & rng I c= Seg m ) ; :: thesis: f (#) g is_partial_differentiable_on Z,b₁
then R721: ( f is_partial_differentiable_on Z,I & g is_partial_differentiable_on Z,I ) by R71, TDef9;
RRRR: 1 <= len I by FINSEQ_1:20;
then T1: 1 in dom I by FINSEQ_3:25;
then T4: I /. 1 = I . 1 by PARTFUN1:def 6;
T2: I . 1 in rng I by T1, FUNCT_1:3;
then I . 1 in Seg m by P72;
then reconsider i = I . 1 as Element of NAT ;
P75: ( 1 <= i & i <= m ) by T2, P72, 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 T3: I = <*(I /. 1)*> by FINSEQ_5:14;
then ( f is_partial_differentiable_on Z,i & g is_partial_differentiable_on Z,i ) by XCW041, R721, T4;
then f (#) g is_partial_differentiable_on Z,i by P75, XXX4, AS;
hence f (#) g is_partial_differentiable_on Z,I by XCW041, T3, T4; :: thesis: verum

end;

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

then 1 < len I by RRRR, 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 RRRR, RFINSEQ:def 1;
then reconsider J = I /^ 1 as non empty FinSequence of NAT by FINSEQ_1:20;
set I1 = <*i*>;
(len I) - 1 <= k by P72, XREAL_1:20;
then P74: len J <= k by RRRR, RFINSEQ:def 1;
V1: I = <*(I /. 1)*> ^ (I /^ 1) by FINSEQ_5:29;
then U1: ( rng <*i*> c= rng I & rng J c= rng I ) by T4, FINSEQ_1:29, FINSEQ_1:30;
then P76: rng J c= Seg m by P72, XBOOLE_1:1;
I = <*i*> ^ J by T4, FINSEQ_5:29;
then ( f is_partial_differentiable_on Z,<*i*> & g is_partial_differentiable_on Z,<*i*> ) by XCW040, R721;
then P79: ( f is_partial_differentiable_on Z,i & g is_partial_differentiable_on Z,i ) by XCW041;
then f (#) g is_partial_differentiable_on Z,i by P75, XXX4, AS;
then P86: f (#) g is_partial_differentiable_on Z,<*i*> by XCW041;
P87: (f (#) g) `partial| (Z,<*i*>) = (f (#) g) `partial| (Z,i) by XCW042
.= ((f `partial| (Z,i)) (#) g) + (f (#) (g `partial| (Z,i))) by P79, P75, XXX4, AS
.= ((f `partial| (Z,<*i*>)) (#) g) + (f (#) (g `partial| (Z,i))) by XCW042
.= ((f `partial| (Z,<*i*>)) (#) g) + (f (#) (g `partial| (Z,<*i*>))) by XCW042 ;
( len <*i*> = 1 & rng <*i*> c= Seg m ) by U1, P72, FINSEQ_1:39, XBOOLE_1:1;
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 XCW0400, R71;
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 P71, R711;
then ( (f `partial| (Z,<*i*>)) (#) g is_partial_differentiable_on Z,J & f (#) (g `partial| (Z,<*i*>)) is_partial_differentiable_on Z,J ) by P74, P76, TDef9;
then ((f `partial| (Z,<*i*>)) (#) g) + (f (#) (g `partial| (Z,<*i*>))) is_partial_differentiable_on Z,J by AS, P76, XCW011;
hence f (#) g is_partial_differentiable_on Z,I by P86, V1, T4, P87, XCW040; :: thesis: verum

end;

end;

end;

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

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(P9, P7);
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