let m be non zero Element of NAT ; :: thesis: for Z being set
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
for n being Nat st n <= len I holds
(PartDiffSeq ((f `partial| (Z,G)),Z,I)) . n = (PartDiffSeq (f,Z,(G ^ I))) . ((len G) + n)
let Z be set ; :: 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
for n being Nat st n <= len I holds
(PartDiffSeq ((f `partial| (Z,G)),Z,I)) . n = (PartDiffSeq (f,Z,(G ^ I))) . ((len G) + n)
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
for n being Nat st n <= len I holds
(PartDiffSeq ((f `partial| (Z,G)),Z,I)) . n = (PartDiffSeq (f,Z,(G ^ I))) . ((len G) + n)
let I, G be non empty FinSequence of NAT ; :: thesis: ( f is_partial_differentiable_on Z,G implies for n being Nat st n <= len I holds
(PartDiffSeq ((f `partial| (Z,G)),Z,I)) . n = (PartDiffSeq (f,Z,(G ^ I))) . ((len G) + n) )
assume A1: f is_partial_differentiable_on Z,G ; :: thesis: for n being Nat st n <= len I holds
(PartDiffSeq ((f `partial| (Z,G)),Z,I)) . n = (PartDiffSeq (f,Z,(G ^ I))) . ((len G) + n)
set g = f `partial| (Z,G);
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 NAT_1:11, FINSEQ_3:25;
1 <= (len G) + (i + 1) by NAT_1:11, XREAL_1:38;
then (len G) + (i + 1) in dom (G ^ I) by A5, A7, XREAL_1:7, FINSEQ_3:25;
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 implies (PartDiffSeq (f,Z,(G ^ I))) . $1 = (PartDiffSeq (f,Z,G)) . $1 );
A9: S1[ 0 ]
proof
assume 0 <= len G ; :: thesis: (PartDiffSeq (f,Z,(G ^ I))) . 0 = (PartDiffSeq (f,Z,G)) . 0
(PartDiffSeq (f,Z,(G ^ I))) . 0 = f | Z by Def7;
hence (PartDiffSeq (f,Z,(G ^ I))) . 0 = (PartDiffSeq (f,Z,G)) . 0 by Def7; :: 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 ; :: thesis: (PartDiffSeq (f,Z,(G ^ I))) . (k + 1) = (PartDiffSeq (f,Z,G)) . (k + 1)
then A122: (k + 1) - 1 <= (len G) - 1 by XREAL_1:9;
k <= k + 1 by NAT_1:11;
then A13: k <= len G by A12, XXREAL_0:2;
thus (PartDiffSeq (f,Z,(G ^ I))) . (k + 1) = ((PartDiffSeq (f,Z,(G ^ I))) . k) `partial| (Z,((G ^ I) /. (k + 1))) by Def7
.= ((PartDiffSeq (f,Z,G)) . k) `partial| (Z,(G /. (k + 1))) by A13, A3, A11, A122
.= (PartDiffSeq (f,Z,G)) . (k + 1) by Def7 ; :: thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch 2(A9, A10);
 then A15: (PartDiffSeq (f,Z,(G ^ I))) . (len G) = (PartDiffSeq (f,Z,G)) . (len G) ;
defpred S2[ Nat] means ( $1 <= len I 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 ; :: 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) = (f `partial| (Z,G)) | Z by A1, A15, Th72;
hence (PartDiffSeq ((f `partial| (Z,G)),Z,I)) . 0 = (PartDiffSeq (f,Z,(G ^ I))) . ((len G) + 0) by Def7; :: 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 ; :: thesis: (PartDiffSeq ((f `partial| (Z,G)),Z,I)) . (k + 1) = (PartDiffSeq (f,Z,(G ^ I))) . ((len G) + (k + 1))
then A199: (k + 1) - 1 <= (len I) - 1 by XREAL_1:9;
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, A199;
(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 Def7;
hence (PartDiffSeq ((f `partial| (Z,G)),Z,I)) . (k + 1) = (PartDiffSeq (f,Z,(G ^ I))) . ((len G) + (k + 1)) by A20, A19, A18, A21, Def7, XXREAL_0:2; :: thesis: verum
end;
for n being Nat holds S2[n] from NAT_1:sch 2(A16, A17);
 hence for n being Nat st n <= len I holds
(PartDiffSeq ((f `partial| (Z,G)),Z,I)) . n = (PartDiffSeq (f,Z,(G ^ I))) . ((len G) + n) ; :: thesis: verum