let S be RealNormSpace-Sequence; :: thesis:
let T be RealNormSpace; :: thesis:
let Z be Subset of (product S); :: thesis:
let I, G be non empty FinSequence of dom S; :: thesis:
let f be PartFunc of (product S),T; :: thesis:
A1: for i being Nat st i < len I holds
(I ^ G) . (i + 1) = I . (i + 1)

let i be Nat; :: thesis:
assume i < len I ; :: thesis:
then ( 1 <= i + 1 & i + 1 <= len I ) by NAT_1:11, NAT_1:13;
then i + 1 in dom I by FINSEQ_3:25;
hence (I ^ G) . (i + 1) = I . (i + 1) by FINSEQ_1:def 7; :: thesis:

end;

A2: len (I ^ G) = (len I) + (len G) by FINSEQ_1:22;
A3: for i being Nat st i < len G holds
(I ^ G) . ((len I) + (i + 1)) = G . (i + 1)

let i be Nat; :: thesis:
assume i < len G ; :: thesis:
then i + 1 <= len G by NAT_1:13;
then i + 1 in dom G by NAT_1:11, FINSEQ_3:25;
hence (I ^ G) . ((len I) + (i + 1)) = G . (i + 1) by FINSEQ_1:def 7; :: thesis:

end;

0 + (len I) < (len G) + (len I) by XREAL_1:8;
then A6: len I < len (I ^ G) by FINSEQ_1:22;
A5: ( 1 <= len I & 1 <= len G ) by FINSEQ_1:20;
then 1 in dom G by FINSEQ_3:25;
then A7: (I ^ G) . ((len I) + 1) = G . 1 by FINSEQ_1:def 7;
A8: 1 <= len I by FINSEQ_1:20;
A9: 1 in dom I by A5, FINSEQ_3:25;

hereby :: thesis:

assume A11: f is_partial_differentiable_on Z,I ^ G ; :: thesis:
for i being Nat st 1 <= i & i < len I holds
PartDiffSeq (f,Z,I,i) is_partial_differentiable_on Z,I . (i + 1)

let i be Nat; :: thesis:
assume A13: ( 1 <= i & i < len I ) ; :: thesis:
then i < len (I ^ G) by A6, XXREAL_0:2;
then A14: PartDiffSeq (f,Z,(I ^ G),i) is_partial_differentiable_on Z,(I ^ G) . (i + 1) by A11, A13;
A15: (I ^ G) . (i + 1) = I . (i + 1) by A1, A13;
Partdiff_SP (S,T,(I ^ G),i) = Partdiff_SP (S,T,I,i) by A13, Th16;
hence PartDiffSeq (f,Z,I,i) is_partial_differentiable_on Z,I . (i + 1) by A13, A14, A15, Th16; :: thesis:

end;

hence f is_partial_differentiable_on Z,I by A9, A11, FINSEQ_1:def 7; :: thesis:
A17: PartDiffSeq (f,Z,(I ^ G),(len I)) is_partial_differentiable_on Z,(I ^ G) . ((len I) + 1) by A6, A11, FINSEQ_1:20;
A18: PartDiffSeq (f,Z,(I ^ G),(len I)) = f `partial| (Z,I) by A8, Th16;
for i being Nat st 1 <= i & i < len G holds
PartDiffSeq ((f `partial| (Z,I)),Z,G,i) is_partial_differentiable_on Z,G . (i + 1)

let i be Nat; :: thesis:
assume A20: ( 1 <= i & i < len G ) ; :: thesis:
then A21: (len I) + i < len (I ^ G) by A2, XREAL_1:8;
A22: 1 + 0 <= (len I) + i by A20, XREAL_1:7;
A23: Partdiff_SP (S,(Partdiff_SP (S,T,I,(len I))),G,i) = Partdiff_SP (S,T,(I ^ G),((len I) + i)) by A20, Th16;
A24: PartDiffSeq ((f `partial| (Z,I)),Z,G,i) = PartDiffSeq (f,Z,(I ^ G),((len I) + i)) by A20, Th16;
(I ^ G) . (((len I) + i) + 1) = (I ^ G) . ((len I) + (i + 1))
.= G . (i + 1) by A3, A20 ;
hence PartDiffSeq ((f `partial| (Z,I)),Z,G,i) is_partial_differentiable_on Z,G . (i + 1) by A11, A21, A22, A23, A24; :: thesis:

end;

hence f `partial| (Z,I) is_partial_differentiable_on Z,G by A7, A8, A17, A18, Th16; :: thesis:

end;

assume that
A25: f is_partial_differentiable_on Z,I and
A26: f `partial| (Z,I) is_partial_differentiable_on Z,G ; :: thesis:
A29: (I ^ G) . (0 + 1) = I . (0 + 1) by A1;
for i being Nat st 1 <= i & i < len (I ^ G) holds
PartDiffSeq (f,Z,(I ^ G),i) is_partial_differentiable_on Z,(I ^ G) . (i + 1)

let i be Nat; :: thesis:
assume A30: ( 1 <= i & i < len (I ^ G) ) ; :: thesis:

suppose A31: i < len I ; :: thesis:

then A32: PartDiffSeq (f,Z,(I ^ G),i) = PartDiffSeq (f,Z,I,i) by A30, Th16;
A33: Partdiff_SP (S,T,(I ^ G),i) = Partdiff_SP (S,T,I,i) by A30, A31, Th16;
PartDiffSeq (f,Z,I,i) is_partial_differentiable_on Z,I . (i + 1) by A25, A30, A31;
hence PartDiffSeq (f,Z,(I ^ G),i) is_partial_differentiable_on Z,(I ^ G) . (i + 1) by A1, A31, A32, A33; :: thesis:

end;

suppose len I <= i ; :: thesis:

then (len I) - (len I) <= i - (len I) by XREAL_1:9;
then i - (len I) in NAT by INT_1:3;
then reconsider j = i - (len I) as Nat ;
A35: j < ((len I) + (len G)) - (len I) by A2, A30, XREAL_1:14;

suppose A36: j = 0 ; :: thesis:

then PartDiffSeq (f,Z,(I ^ G),i) = f `partial| (Z,I) by A30, Th16;
hence PartDiffSeq (f,Z,(I ^ G),i) is_partial_differentiable_on Z,(I ^ G) . (i + 1) by A7, A26, A30, A36, Th16; :: thesis:

end;

suppose A38: j <> 0 ; :: thesis:

then A39: 1 <= j by NAT_1:14;
A40: PartDiffSeq ((f `partial| (Z,I)),Z,G,j) is_partial_differentiable_on Z,G . (j + 1) by A26, A35, A38, NAT_1:14;
A41: (I ^ G) . (i + 1) = (I ^ G) . ((len I) + (j + 1))
.= G . (j + 1) by A3, A35 ;
Partdiff_SP (S,(Partdiff_SP (S,T,I,(len I))),G,j) = Partdiff_SP (S,T,(I ^ G),((len I) + j)) by A35, A39, Th16;
hence PartDiffSeq (f,Z,(I ^ G),i) is_partial_differentiable_on Z,(I ^ G) . (i + 1) by A35, A39, A40, A41, Th16; :: thesis:

end;

end;

end;

end;

end;

hence f is_partial_differentiable_on Z,I ^ G by A25, A29; :: thesis: