let m be non zero Element of NAT ; :: thesis: for Z being non empty Subset of (REAL m)
for f being PartFunc of (REAL m),REAL
for I, G being non empty FinSequence of NAT st f is_partial_differentiable_on Z,G holds
f `partial| (Z,(G ^ I)) = (f `partial| (Z,G)) `partial| (Z,I)
let Z be non empty Subset of (REAL m); :: thesis: for f being PartFunc of (REAL m),REAL
for I, G being non empty FinSequence of NAT st f is_partial_differentiable_on Z,G holds
f `partial| (Z,(G ^ I)) = (f `partial| (Z,G)) `partial| (Z,I)
let f be PartFunc of (REAL m),REAL; :: thesis: for I, G being non empty FinSequence of NAT st f is_partial_differentiable_on Z,G holds
f `partial| (Z,(G ^ I)) = (f `partial| (Z,G)) `partial| (Z,I)
let I, G be non empty FinSequence of NAT ; :: thesis: ( f is_partial_differentiable_on Z,G implies f `partial| (Z,(G ^ I)) = (f `partial| (Z,G)) `partial| (Z,I) )
set g = f `partial| (Z,G);
reconsider Z0 = 0 as Element of NAT ;
assume A1: f is_partial_differentiable_on Z,G ; :: thesis: f `partial| (Z,(G ^ I)) = (f `partial| (Z,G)) `partial| (Z,I)
A2: dom G c= dom (G ^ I) by FINSEQ_1:26;
A3: for i being Nat st i <= (len G) - 1 holds
(G ^ I) /. (i + 1) = G /. (i + 1)
proof
let i be Nat; :: thesis: ( i <= (len G) - 1 implies (G ^ I) /. (i + 1) = G /. (i + 1) )
assume i <= (len G) - 1 ; :: thesis: (G ^ I) /. (i + 1) = G /. (i + 1)
then ( 1 <= i + 1 & i + 1 <= len G ) by NAT_1:11, XREAL_1:19;
then A4: i + 1 in dom G by FINSEQ_3:25;
then (G ^ I) /. (i + 1) = (G ^ I) . (i + 1) by A2, PARTFUN1:def 6;
then (G ^ I) /. (i + 1) = G . (i + 1) by A4, FINSEQ_1:def 7;
hence (G ^ I) /. (i + 1) = G /. (i + 1) by A4, PARTFUN1:def 6; :: thesis: verum
end;
A5: len (G ^ I) = (len G) + (len I) by FINSEQ_1:22;
A6: for i being Nat st i <= (len I) - 1 holds
(G ^ I) /. ((len G) + (i + 1)) = I /. (i + 1)
proof
let i be Nat; :: thesis: ( i <= (len I) - 1 implies (G ^ I) /. ((len G) + (i + 1)) = I /. (i + 1) )
assume i <= (len I) - 1 ; :: thesis: (G ^ I) /. ((len G) + (i + 1)) = I /. (i + 1)
then A7: i + 1 <= len I by XREAL_1:19;
then A8: i + 1 in dom I by FINSEQ_3:25, NAT_1:11;
1 <= (len G) + (i + 1) by NAT_1:11, XREAL_1:38;
then (len G) + (i + 1) in dom (G ^ I) by FINSEQ_3:25, A5, A7, XREAL_1:7;
hence (G ^ I) /. ((len G) + (i + 1)) = (G ^ I) . ((len G) + (i + 1)) by PARTFUN1:def 6
.= I . (i + 1) by A8, FINSEQ_1:def 7
.= I /. (i + 1) by A8, PARTFUN1:def 6 ;
:: thesis: verum
end;
defpred S1[ Nat] means ( $1 <= (len G) - 1 implies (PartDiffSeq (f,Z,(G ^ I))) . $1 = (PartDiffSeq (f,Z,G)) . $1 );
A9: S1[ 0 ]
proof
assume 0 <= (len G) - 1 ; :: thesis: (PartDiffSeq (f,Z,(G ^ I))) . 0 = (PartDiffSeq (f,Z,G)) . 0
(PartDiffSeq (f,Z,(G ^ I))) . 0 = f | Z by PDIFF_9:def 7;
hence (PartDiffSeq (f,Z,(G ^ I))) . 0 = (PartDiffSeq (f,Z,G)) . 0 by PDIFF_9:def 7; :: thesis: verum
end;
A10: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A11: S1[k] ; :: thesis: S1[k + 1]
assume A12: k + 1 <= (len G) - 1 ; :: thesis: (PartDiffSeq (f,Z,(G ^ I))) . (k + 1) = (PartDiffSeq (f,Z,G)) . (k + 1)
A13: k <= k + 1 by NAT_1:11;
thus (PartDiffSeq (f,Z,(G ^ I))) . (k + 1) = ((PartDiffSeq (f,Z,(G ^ I))) . k) `partial| (Z,((G ^ I) /. (k + 1))) by PDIFF_9:def 7
.= ((PartDiffSeq (f,Z,G)) . k) `partial| (Z,(G /. (k + 1))) by A13, A3, A11, A12, XXREAL_0:2
.= (PartDiffSeq (f,Z,G)) . (k + 1) by PDIFF_9:def 7 ; :: thesis: verum
end;
A14: for n being Nat holds S1[n] from NAT_1:sch 2(A9, A10);
 reconsider j = (len G) - 1 as Element of NAT by INT_1:5, FINSEQ_1:20;
A15: (PartDiffSeq (f,Z,(G ^ I))) . (len G) = ((PartDiffSeq (f,Z,(G ^ I))) . j) `partial| (Z,((G ^ I) /. (j + 1))) by PDIFF_9:def 7
.= ((PartDiffSeq (f,Z,G)) . j) `partial| (Z,((G ^ I) /. (j + 1))) by A14
.= ((PartDiffSeq (f,Z,G)) . j) `partial| (Z,(G /. (j + 1))) by A3
.= (PartDiffSeq (f,Z,G)) . (len G) by PDIFF_9:def 7 ;
defpred S2[ Nat] means ( $1 <= (len I) - 1 implies (PartDiffSeq ((f `partial| (Z,G)),Z,I)) . $1 = (PartDiffSeq (f,Z,(G ^ I))) . ((len G) + $1) );
A16: S2[ 0 ]
proof
assume 0 <= (len I) - 1 ; :: thesis: (PartDiffSeq ((f `partial| (Z,G)),Z,I)) . 0 = (PartDiffSeq (f,Z,(G ^ I))) . ((len G) + 0)
(PartDiffSeq (f,Z,(G ^ I))) . ((len G) + 0) = (PartDiffSeq (f,Z,G)) . (len G) by A15
.= f `partial| (Z,G)
.= (f `partial| (Z,G)) | Z by PDIFF_9:72, A1
.= (PartDiffSeq ((f `partial| (Z,G)),Z,I)) . 0 by PDIFF_9:def 7 ;
hence (PartDiffSeq ((f `partial| (Z,G)),Z,I)) . 0 = (PartDiffSeq (f,Z,(G ^ I))) . ((len G) + 0) ; :: thesis: verum
end;
A17: for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
assume A18: S2[k] ; :: thesis: S2[k + 1]
set i = (len G) + k;
assume A19: k + 1 <= (len I) - 1 ; :: thesis: (PartDiffSeq ((f `partial| (Z,G)),Z,I)) . (k + 1) = (PartDiffSeq (f,Z,(G ^ I))) . ((len G) + (k + 1))
A20: k <= k + 1 by NAT_1:11;
(G ^ I) /. (((len G) + k) + 1) = (G ^ I) /. ((len G) + (k + 1)) ;
then A21: (G ^ I) /. (((len G) + k) + 1) = I /. (k + 1) by A6, A20, A19, XXREAL_0:2;
(PartDiffSeq (f,Z,(G ^ I))) . ((len G) + (k + 1)) = ((PartDiffSeq (f,Z,(G ^ I))) . ((len G) + k)) `partial| (Z,((G ^ I) /. (((len G) + k) + 1))) by PDIFF_9:def 7;
hence (PartDiffSeq ((f `partial| (Z,G)),Z,I)) . (k + 1) = (PartDiffSeq (f,Z,(G ^ I))) . ((len G) + (k + 1)) by A20, A19, A18, A21, PDIFF_9:def 7, XXREAL_0:2; :: thesis: verum
end;
A22: for n being Nat holds S2[n] from NAT_1:sch 2(A16, A17);
 reconsider j0 = (len I) - 1 as Element of NAT by INT_1:5, FINSEQ_1:20;
reconsider j1 = (len (G ^ I)) - 1 as Element of NAT by INT_1:5, FINSEQ_1:20;
A23: j1 = (len G) + j0 by A5;
f `partial| (Z,(G ^ I)) = ((PartDiffSeq (f,Z,(G ^ I))) . j1) `partial| (Z,((G ^ I) /. (j1 + 1))) by PDIFF_9:def 7
.= ((PartDiffSeq ((f `partial| (Z,G)),Z,I)) . j0) `partial| (Z,((G ^ I) /. ((len G) + (j0 + 1)))) by A22, A23
.= ((PartDiffSeq ((f `partial| (Z,G)),Z,I)) . j0) `partial| (Z,(I /. (j0 + 1))) by A6
.= (f `partial| (Z,G)) `partial| (Z,I) by PDIFF_9:def 7 ;
hence f `partial| (Z,(G ^ I)) = (f `partial| (Z,G)) `partial| (Z,I) ; :: thesis: verum