let m be non zero Element of NAT ; for X being Subset of (REAL m)
for r being Real
for I being non empty FinSequence of NAT
for f being PartFunc of (REAL m),REAL st X is open & rng I c= Seg m & f is_partial_differentiable_on X,I holds
for i being Element of NAT st i <= (len I) - 1 holds
( (PartDiffSeq ((r (#) f),X,I)) . i is_partial_differentiable_on X,I /. (i + 1) & (PartDiffSeq ((r (#) f),X,I)) . i = r (#) ((PartDiffSeq (f,X,I)) . i) )
let Z be Subset of (REAL m); for r being Real
for I being non empty FinSequence of NAT
for f being PartFunc of (REAL m),REAL st Z is open & rng I c= Seg m & f is_partial_differentiable_on Z,I holds
for i being Element of NAT st i <= (len I) - 1 holds
( (PartDiffSeq ((r (#) f),Z,I)) . i is_partial_differentiable_on Z,I /. (i + 1) & (PartDiffSeq ((r (#) f),Z,I)) . i = r (#) ((PartDiffSeq (f,Z,I)) . i) )
let r be Real; for I being non empty FinSequence of NAT
for f being PartFunc of (REAL m),REAL st Z is open & rng I c= Seg m & f is_partial_differentiable_on Z,I holds
for i being Element of NAT st i <= (len I) - 1 holds
( (PartDiffSeq ((r (#) f),Z,I)) . i is_partial_differentiable_on Z,I /. (i + 1) & (PartDiffSeq ((r (#) f),Z,I)) . i = r (#) ((PartDiffSeq (f,Z,I)) . i) )
let I be non empty FinSequence of NAT ; for f being PartFunc of (REAL m),REAL st Z is open & rng I c= Seg m & f is_partial_differentiable_on Z,I holds
for i being Element of NAT st i <= (len I) - 1 holds
( (PartDiffSeq ((r (#) f),Z,I)) . i is_partial_differentiable_on Z,I /. (i + 1) & (PartDiffSeq ((r (#) f),Z,I)) . i = r (#) ((PartDiffSeq (f,Z,I)) . i) )
let f be PartFunc of (REAL m),REAL; ( Z is open & rng I c= Seg m & f is_partial_differentiable_on Z,I implies for i being Element of NAT st i <= (len I) - 1 holds
( (PartDiffSeq ((r (#) f),Z,I)) . i is_partial_differentiable_on Z,I /. (i + 1) & (PartDiffSeq ((r (#) f),Z,I)) . i = r (#) ((PartDiffSeq (f,Z,I)) . i) ) )
assume A1:
( Z is open & rng I c= Seg m & f is_partial_differentiable_on Z,I )
; for i being Element of NAT st i <= (len I) - 1 holds
( (PartDiffSeq ((r (#) f),Z,I)) . i is_partial_differentiable_on Z,I /. (i + 1) & (PartDiffSeq ((r (#) f),Z,I)) . i = r (#) ((PartDiffSeq (f,Z,I)) . i) )
defpred S1[ Nat] means ( $1 <= (len I) - 1 implies ( (PartDiffSeq ((r (#) f),Z,I)) . $1 is_partial_differentiable_on Z,I /. ($1 + 1) & (PartDiffSeq ((r (#) f),Z,I)) . $1 = r (#) ((PartDiffSeq (f,Z,I)) . $1) ) );
reconsider Z0 = 0 as Element of NAT ;
A2:
S1[ 0 ]
proof
assume
0 <= (len I) - 1
;
( (PartDiffSeq ((r (#) f),Z,I)) . 0 is_partial_differentiable_on Z,I /. (0 + 1) & (PartDiffSeq ((r (#) f),Z,I)) . 0 = r (#) ((PartDiffSeq (f,Z,I)) . 0) )
then A3:
(PartDiffSeq (f,Z,I)) . Z0 is_partial_differentiable_on Z,
I /. (Z0 + 1)
by A1;
A4:
(r (#) f) | Z = r (#) (f | Z)
by RFUNCT_1:49;
(PartDiffSeq ((r (#) f),Z,I)) . Z0 = (r (#) f) | Z
by Def7;
then A5:
(PartDiffSeq ((r (#) f),Z,I)) . Z0 = r (#) ((PartDiffSeq (f,Z,I)) . Z0)
by A4, Def7;
1
<= len I
by FINSEQ_1:20;
then
I /. 1
in Seg m
by A1, Lm6;
then
( 1
<= I /. 1 &
I /. 1
<= m )
by FINSEQ_1:1;
hence
(
(PartDiffSeq ((r (#) f),Z,I)) . 0 is_partial_differentiable_on Z,
I /. (0 + 1) &
(PartDiffSeq ((r (#) f),Z,I)) . 0 = r (#) ((PartDiffSeq (f,Z,I)) . 0) )
by A5, A1, A3, Th67;
verum
end;
A6:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A7:
S1[
k]
;
S1[k + 1]
assume A8:
k + 1
<= (len I) - 1
;
( (PartDiffSeq ((r (#) f),Z,I)) . (k + 1) is_partial_differentiable_on Z,I /. ((k + 1) + 1) & (PartDiffSeq ((r (#) f),Z,I)) . (k + 1) = r (#) ((PartDiffSeq (f,Z,I)) . (k + 1)) )
A9:
k <= k + 1
by NAT_1:11;
then A10:
k <= (len I) - 1
by A8, XXREAL_0:2;
A11:
(PartDiffSeq (f,Z,I)) . (k + 1) is_partial_differentiable_on Z,
I /. ((k + 1) + 1)
by A8, A1;
k + 1
<= ((len I) - 1) + 1
by A10, XREAL_1:6;
then
I /. (k + 1) in Seg m
by A1, Lm6, NAT_1:11;
then A12:
( 1
<= I /. (k + 1) &
I /. (k + 1) <= m )
by FINSEQ_1:1;
k in NAT
by ORDINAL1:def 12;
then A13:
(PartDiffSeq (f,Z,I)) . k is_partial_differentiable_on Z,
I /. (k + 1)
by A1, A9, A8, XXREAL_0:2;
(k + 1) + 1
<= ((len I) - 1) + 1
by A8, XREAL_1:6;
then
I /. ((k + 1) + 1) in Seg m
by A1, Lm6, NAT_1:11;
then A14:
( 1
<= I /. ((k + 1) + 1) &
I /. ((k + 1) + 1) <= m )
by FINSEQ_1:1;
A15:
(PartDiffSeq ((r (#) f),Z,I)) . (k + 1) =
(r (#) ((PartDiffSeq (f,Z,I)) . k)) `partial| (
Z,
(I /. (k + 1)))
by A9, A8, A7, Def7, XXREAL_0:2
.=
r (#) (((PartDiffSeq (f,Z,I)) . k) `partial| (Z,(I /. (k + 1))))
by A13, A1, A12, Th67
.=
r (#) ((PartDiffSeq (f,Z,I)) . (k + 1))
by Def7
;
hence
(PartDiffSeq ((r (#) f),Z,I)) . (k + 1) is_partial_differentiable_on Z,
I /. ((k + 1) + 1)
by A1, A11, A14, Th67;
(PartDiffSeq ((r (#) f),Z,I)) . (k + 1) = r (#) ((PartDiffSeq (f,Z,I)) . (k + 1))
thus
(PartDiffSeq ((r (#) f),Z,I)) . (k + 1) = r (#) ((PartDiffSeq (f,Z,I)) . (k + 1))
by A15;
verum
end;
for n being Nat holds S1[n]
from NAT_1:sch 2(A2, A6);
hence
for i being Element of NAT st i <= (len I) - 1 holds
( (PartDiffSeq ((r (#) f),Z,I)) . i is_partial_differentiable_on Z,I /. (i + 1) & (PartDiffSeq ((r (#) f),Z,I)) . i = r (#) ((PartDiffSeq (f,Z,I)) . i) )
; verum