let m be non zero Element of NAT ; :: thesis: 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); :: thesis: 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; :: thesis: 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 ; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: 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 S₁[ 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: S₁[ 0 ]

proof

assume 0 <= (len I) - 1 ; :: thesis: ( (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; :: thesis: verum

end;

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

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A7: S₁[k] ; :: thesis: S₁[k + 1]
assume A8: k + 1 <= (len I) - 1 ; :: thesis: ( (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; :: thesis: (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; :: thesis: verum

end;

for n being Nat holds S₁[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) ) ; :: thesis: verum