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

proof

let f, g be PartFunc of (REAL m),REAL; :: thesis: ( f is_continuously_differentiable_up_to_order 0 ,Z & g is_continuously_differentiable_up_to_order 0 ,Z implies f (#) g is_continuously_differentiable_up_to_order 0 ,Z )
assume A3: ( f is_continuously_differentiable_up_to_order 0 ,Z & g is_continuously_differentiable_up_to_order 0 ,Z ) ; :: thesis: f (#) g is_continuously_differentiable_up_to_order 0 ,Z
dom (f (#) g) = (dom f) /\ (dom g) by VALUED_1:def 4;
hence f (#) g is_continuously_differentiable_up_to_order 0 ,Z by A3, XBOOLE_1:19, FINSEQ_1:20, PDIFF_9:87, A1; :: thesis: verum

end;

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

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: S₁[k] ; :: thesis: S₁[k + 1]
let f, g be PartFunc of (REAL m),REAL; :: thesis: ( f is_continuously_differentiable_up_to_order k + 1,Z & g is_continuously_differentiable_up_to_order k + 1,Z implies f (#) g is_continuously_differentiable_up_to_order k + 1,Z )
assume A6: ( f is_continuously_differentiable_up_to_order k + 1,Z & g is_continuously_differentiable_up_to_order k + 1,Z ) ; :: thesis: f (#) g is_continuously_differentiable_up_to_order k + 1,Z
then A7: ( f is_continuously_differentiable_up_to_order k,Z & g is_continuously_differentiable_up_to_order k,Z ) by Th10, NAT_1:11;
dom (f (#) g) = (dom f) /\ (dom g) by VALUED_1:def 4;
then A8: Z c= dom (f (#) g) by A6, XBOOLE_1:19;

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

let I be non empty FinSequence of NAT ; :: thesis: ( len I <= k + 1 & rng I c= Seg m implies (f (#) g) `partial| (Z,b<sub>1</sub>) is_continuous_on Z )
assume A9: ( len I <= k + 1 & rng I c= Seg m ) ; :: thesis: (f (#) g) `partial| (Z,b₁) is_continuous_on Z
then A10: ( f is_partial_differentiable_on Z,I & g is_partial_differentiable_on Z,I ) by PDIFF_9:def 11, A6;
A11: ( f `partial| (Z,I) is_continuous_on Z & g `partial| (Z,I) is_continuous_on Z ) by A9, A6;
A12: 1 <= len I by FINSEQ_1:20;
then A13: 1 in dom I by FINSEQ_3:25;
then A14: I /. 1 = I . 1 by PARTFUN1:def 6;
A15: I . 1 in rng I by A13, FUNCT_1:3;
reconsider i = I . 1 as Element of NAT by ORDINAL1:def 12;
A16: ( 1 <= i & i <= m ) by A15, A9, FINSEQ_1:1;

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

suppose A17: 1 = len I ; :: thesis: (f (#) g) `partial| (Z,b₁) is_continuous_on Z

then A18: I = <*(I . 1)*> by FINSEQ_5:14;
A19: f (#) g is_continuously_differentiable_up_to_order k,Z by A5, A7;

now :: thesis: (f (#) g) `partial| (Z,I) is_continuous_on Z

per cases ( k = 0 or k <> 0 ) ;

suppose A20: k = 0 ; :: thesis: (f (#) g) `partial| (Z,I) is_continuous_on Z

A21: I = <*i*> by A17, FINSEQ_5:14;
A22: ( f is_partial_differentiable_on Z,i & g is_partial_differentiable_on Z,i ) by A18, A9, PDIFF_9:def 11, A6;
then A23: (f (#) g) `partial| (Z,I) = (f (#) g) `partial| (Z,i) by A1, A16, A21, PDIFF_9:68, PDIFF_9:82
.= ((f `partial| (Z,i)) (#) g) + (f (#) (g `partial| (Z,i))) by A1, A22, A16, PDIFF_9:68
.= ((f `partial| (Z,I)) (#) g) + (f (#) (g `partial| (Z,i))) by A1, A16, A21, A22, PDIFF_9:82
.= ((f `partial| (Z,I)) (#) g) + (f (#) (g `partial| (Z,I))) by A1, A16, A21, A22, PDIFF_9:82 ;
A24: ( Z c= dom (f `partial| (Z,I)) & Z c= dom (g `partial| (Z,I)) ) by A9, Th1, PDIFF_9:def 11, A6;
A25: f is_continuous_on Z by A1, Th3, A6, A20;
g is_continuous_on Z by A1, Th3, A6, A20;
then A26: (f `partial| (Z,I)) (#) g is_continuous_on Z by A11, A6, A24, PDIFF_9:48;
A27: f (#) (g `partial| (Z,I)) is_continuous_on Z by A11, A25, A6, A24, PDIFF_9:48;
dom ((f `partial| (Z,I)) (#) g) = (dom (f `partial| (Z,I))) /\ (dom g) by VALUED_1:def 4;
then A28: Z c= dom ((f `partial| (Z,I)) (#) g) by A24, A6, XBOOLE_1:19;
dom (f (#) (g `partial| (Z,I))) = (dom f) /\ (dom (g `partial| (Z,I))) by VALUED_1:def 4;
then Z c= dom (f (#) (g `partial| (Z,I))) by A24, A6, XBOOLE_1:19;
hence (f (#) g) `partial| (Z,I) is_continuous_on Z by A23, A26, A27, A28, PDIFF_9:46; :: thesis: verum

end;

suppose k <> 0 ; :: thesis: (f (#) g) `partial| (Z,I) is_continuous_on Z

hence (f (#) g) `partial| (Z,I) is_continuous_on Z by A19, A9, A17, NAT_1:14; :: thesis: verum

end;

end;

end;

hence (f (#) g) `partial| (Z,I) is_continuous_on Z ; :: thesis: verum

end;

suppose 1 <> len I ; :: thesis: (f (#) g) `partial| (Z,b₁) is_continuous_on Z

then 1 < len I by A12, 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 A12, 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 A9, XREAL_1:20;
then A29: len J <= k by A12, RFINSEQ:def 1;
A30: I = <*(I /. 1)*> ^ (I /^ 1) by FINSEQ_5:29;
then A31: ( rng <*i*> c= rng I & rng J c= rng I ) by A14, FINSEQ_1:29, FINSEQ_1:30;
then A32: rng J c= Seg m by A9;
I = <*i*> ^ J by A14, FINSEQ_5:29;
then A33: ( f is_partial_differentiable_on Z,i & g is_partial_differentiable_on Z,i ) by PDIFF_9:80, A10;
then A34: f (#) g is_partial_differentiable_on Z,i by A1, A16, PDIFF_9:68;
then A35: (f (#) g) `partial| (Z,<*i*>) = (f (#) g) `partial| (Z,i) by A1, A16, PDIFF_9:82
.= ((f `partial| (Z,i)) (#) g) + (f (#) (g `partial| (Z,i))) by A33, A16, PDIFF_9:68, A1
.= ((f `partial| (Z,<*i*>)) (#) g) + (f (#) (g `partial| (Z,i))) by A1, A16, A33, PDIFF_9:82
.= ((f `partial| (Z,<*i*>)) (#) g) + (f (#) (g `partial| (Z,<*i*>))) by A1, A16, A33, PDIFF_9:82 ;
( len <*i*> = 1 & rng <*i*> c= Seg m ) by A31, A9, FINSEQ_1:39;
then ( f `partial| (Z,<*i*>) is_continuously_differentiable_up_to_order k,Z & g `partial| (Z,<*i*>) is_continuously_differentiable_up_to_order k,Z ) by Th9, A6;
then A36: ( (f `partial| (Z,<*i*>)) (#) g is_continuously_differentiable_up_to_order k,Z & f (#) (g `partial| (Z,<*i*>)) is_continuously_differentiable_up_to_order k,Z ) by A5, A7;
then ( (f `partial| (Z,<*i*>)) (#) g is_partial_differentiable_on Z,J & f (#) (g `partial| (Z,<*i*>)) is_partial_differentiable_on Z,J ) by A29, A32, PDIFF_9:def 11;
then A37: (((f `partial| (Z,<*i*>)) (#) g) + (f (#) (g `partial| (Z,<*i*>)))) `partial| (Z,J) = (((f `partial| (Z,<*i*>)) (#) g) `partial| (Z,J)) + ((f (#) (g `partial| (Z,<*i*>))) `partial| (Z,J)) by A1, A32, PDIFF_9:75;
A38: ( Z c= dom (((f `partial| (Z,<*i*>)) (#) g) `partial| (Z,J)) & Z c= dom ((f (#) (g `partial| (Z,<*i*>))) `partial| (Z,J)) ) by A36, Th1, A29, A32, PDIFF_9:def 11;
( ((f `partial| (Z,<*i*>)) (#) g) `partial| (Z,J) is_continuous_on Z & (f (#) (g `partial| (Z,<*i*>))) `partial| (Z,J) is_continuous_on Z ) by A36, A29, A9, XBOOLE_1:1, A31;
then (((f `partial| (Z,<*i*>)) (#) g) + (f (#) (g `partial| (Z,<*i*>)))) `partial| (Z,J) is_continuous_on Z by A37, A38, PDIFF_9:46;
hence (f (#) g) `partial| (Z,I) is_continuous_on Z by A30, A14, A34, A35, Th7; :: thesis: verum

end;

end;

end;

hence f (#) g is_continuously_differentiable_up_to_order k + 1,Z by A8, PDIFF_9:87, A1, A6; :: thesis: verum

end;

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