let m be non zero Element of NAT ; 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); ( 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
; 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 S1[ 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:
S1[ 0 ]
proof
let f,
g be
PartFunc of
(REAL m),
REAL;
( 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 )
;
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;
verum
end;
A4:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A5:
S1[
k]
;
S1[k + 1]
let f,
g be
PartFunc of
(REAL m),
REAL;
( 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 )
;
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 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 Zlet I be non
empty FinSequence of
NAT ;
( len I <= k + 1 & rng I c= Seg m implies (f (#) g) `partial| (Z,b1) is_continuous_on Z )assume A9:
(
len I <= k + 1 &
rng I c= Seg m )
;
(f (#) g) `partial| (Z,b1) is_continuous_on Zthen 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
;
(f (#) g) `partial| (Z,b1) is_continuous_on Zthen A18:
I = <*(I . 1)*>
by FINSEQ_5:14;
A19:
f (#) g is_continuously_differentiable_up_to_order k,
Z
by A5, A7;
now (f (#) g) `partial| (Z,I) is_continuous_on Zper cases
( k = 0 or k <> 0 )
;
suppose A20:
k = 0
;
(f (#) g) `partial| (Z,I) is_continuous_on ZA21:
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;
verum end; end; end; hence
(f (#) g) `partial| (
Z,
I)
is_continuous_on Z
;
verum end; suppose
1
<> len I
;
(f (#) g) `partial| (Z,b1) is_continuous_on Zthen
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;
verum end; end; end;
hence
f (#) g is_continuously_differentiable_up_to_order k + 1,
Z
by A8, PDIFF_9:87, A1, A6;
verum
end;
for n being Nat holds S1[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
; verum