let m be non zero Element of NAT ; :: thesis:
let Z be set ; :: thesis:
let f be PartFunc of (REAL m),REAL; :: thesis:
let I, G be non empty FinSequence of NAT ; :: thesis:
set g = f `partial| (Z,G);
A1: dom G c= dom (G ^ I) by FINSEQ_1:26;
A2: for i being Nat st i <= (len G) - 1 holds
(G ^ I) /. (i + 1) = G /. (i + 1)

let i be Nat; :: thesis:
assume i <= (len G) - 1 ; :: thesis:
then ( 1 <= i + 1 & i + 1 <= len G ) by NAT_1:11, XREAL_1:19;
then A3: i + 1 in dom G by FINSEQ_3:25;
then (G ^ I) /. (i + 1) = (G ^ I) . (i + 1) by A1, PARTFUN1:def 6;
then (G ^ I) /. (i + 1) = G . (i + 1) by A3, FINSEQ_1:def 7;
hence (G ^ I) /. (i + 1) = G /. (i + 1) by A3, PARTFUN1:def 6; :: thesis:

end;

A4: len (G ^ I) = (len G) + (len I) by FINSEQ_1:22;
A5: for i being Nat st i <= (len I) - 1 holds
(G ^ I) /. ((len G) + (i + 1)) = I /. (i + 1)

let i be Nat; :: thesis:
assume i <= (len I) - 1 ; :: thesis:
then A6: i + 1 <= len I by XREAL_1:19;
then A7: 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 A4, A6, FINSEQ_3:25, XREAL_1:7;
hence (G ^ I) /. ((len G) + (i + 1)) = (G ^ I) . ((len G) + (i + 1)) by PARTFUN1:def 6
.= I . (i + 1) by A7, FINSEQ_1:def 7
.= I /. (i + 1) by A7, PARTFUN1:def 6 ;
:: thesis:

end;

defpred S₁[ Nat] means ( $1 <= (len G) - 1 implies (PartDiffSeq (f,Z,(G ^ I))) . $1 = (PartDiffSeq (f,Z,G)) . $1 );
A8: S₁[ 0 ]

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

end;

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

let k be Nat; :: thesis:
assume A10: S₁[k] ; :: thesis:
assume A11: k + 1 <= (len G) - 1 ; :: thesis:
A12: 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 Def7
.= ((PartDiffSeq (f,Z,G)) . k) `partial| (Z,(G /. (k + 1))) by A12, A2, A10, A11, XXREAL_0:2
.= (PartDiffSeq (f,Z,G)) . (k + 1) by Def7 ; :: thesis:

end;

A13: for n being Nat holds S₁[n] from NAT_1:sch 2(A8, A9);

hereby :: thesis:

assume A14: f is_partial_differentiable_on Z,G ^ I ; :: thesis:

let i be Element of NAT ; :: thesis:
assume A15: i <= (len G) - 1 ; :: thesis:
then i + 0 <= ((len G) - 1) + (len I) by XREAL_1:7;
then A16: (PartDiffSeq (f,Z,(G ^ I))) . i is_partial_differentiable_on Z,(G ^ I) /. (i + 1) by A4, A14;
(G ^ I) /. (i + 1) = G /. (i + 1) by A15, A2;
hence (PartDiffSeq (f,Z,G)) . i is_partial_differentiable_on Z,G /. (i + 1) by A16, A15, A13; :: thesis:

end;

hence A17: f is_partial_differentiable_on Z,G ; :: thesis:

let i be Element of NAT ; :: thesis:
assume A18: i <= (len I) - 1 ; :: thesis:
then (len G) + i <= (len G) + ((len I) - 1) by XREAL_1:6;
then A19: (PartDiffSeq (f,Z,(G ^ I))) . ((len G) + i) is_partial_differentiable_on Z,(G ^ I) /. (((len G) + i) + 1) by A4, A14;
(len I) - 1 <= (len I) - 0 by XREAL_1:13;
then A20: i <= len I by A18, XXREAL_0:2;
(G ^ I) /. (((len G) + i) + 1) = (G ^ I) /. ((len G) + (i + 1)) ;
then (G ^ I) /. (((len G) + i) + 1) = I /. (i + 1) by A18, A5;
hence (PartDiffSeq ((f `partial| (Z,G)),Z,I)) . i is_partial_differentiable_on Z,I /. (i + 1) by A19, A20, Th73, A17; :: thesis:

end;

hence f `partial| (Z,G) is_partial_differentiable_on Z,I ; :: thesis:

end;

assume A20: ( f is_partial_differentiable_on Z,G & f `partial| (Z,G) is_partial_differentiable_on Z,I ) ; :: thesis:

let i be Element of NAT ; :: thesis:
assume A21: i <= (len (G ^ I)) - 1 ; :: thesis:

suppose A22: i <= (len G) - 1 ; :: thesis:

then A23: (PartDiffSeq (f,Z,G)) . i is_partial_differentiable_on Z,G /. (i + 1) by A20;
G /. (i + 1) = (G ^ I) /. (i + 1) by A22, A2;
hence (PartDiffSeq (f,Z,(G ^ I))) . i is_partial_differentiable_on Z,(G ^ I) /. (i + 1) by A22, A13, A23; :: thesis:

end;

suppose not i <= (len G) - 1 ; :: thesis:

then len G < i + 1 by XREAL_1:19;
then len G <= i by NAT_1:13;
then reconsider k = i - (len G) as Element of NAT by INT_1:5;
A24: i - (len G) <= (((len G) + (len I)) - 1) - (len G) by A21, A4, XREAL_1:9;
then A25: ( k <= (len I) - 1 & i = k + (len G) ) ;
A26: (PartDiffSeq ((f `partial| (Z,G)),Z,I)) . k is_partial_differentiable_on Z,I /. (k + 1) by A20, A24;
(len I) - 1 <= (len I) - 0 by XREAL_1:13;
then A27: k <= len I by A24, XXREAL_0:2;
i + 1 = (k + 1) + (len G) ;
then I /. (k + 1) = (G ^ I) /. (i + 1) by A24, A5;
hence (PartDiffSeq (f,Z,(G ^ I))) . i is_partial_differentiable_on Z,(G ^ I) /. (i + 1) by A20, A26, A25, A27, Th73; :: thesis:

end;

end;

end;

hence f is_partial_differentiable_on Z,G ^ I ; :: thesis:

end;

hence ( f is_partial_differentiable_on Z,G & f `partial| (Z,G) is_partial_differentiable_on Z,I implies f is_partial_differentiable_on Z,G ^ I ) ; :: thesis: