let m be non empty 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 holds
( f is_partial_differentiable_on Z,G ^ I iff ( f is_partial_differentiable_on Z,G & f `partial| (Z,G) is_partial_differentiable_on Z,I ) )
let Z be set ; :: thesis: for f being PartFunc of (REAL m),REAL
for I, G being non empty FinSequence of NAT holds
( f is_partial_differentiable_on Z,G ^ I iff ( f is_partial_differentiable_on Z,G & f `partial| (Z,G) is_partial_differentiable_on Z,I ) )
let f be PartFunc of (REAL m),REAL; :: thesis: for I, G being non empty FinSequence of NAT holds
( f is_partial_differentiable_on Z,G ^ I iff ( f is_partial_differentiable_on Z,G & f `partial| (Z,G) is_partial_differentiable_on Z,I ) )
let I, G be non empty FinSequence of NAT ; :: thesis: ( f is_partial_differentiable_on Z,G ^ I iff ( f is_partial_differentiable_on Z,G & f `partial| (Z,G) is_partial_differentiable_on Z,I ) )
set g = f `partial| (Z,G);
reconsider Z0 = 0 as Element of NAT ;
S1: dom G c= dom (G ^ I) by FINSEQ_1:26;
Y0: for i being Element of NAT st i <= (len G) - 1 holds
(G ^ I) /. (i + 1) = G /. (i + 1)
proof
let i be Element of 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 D3: i + 1 in dom G by FINSEQ_3:25;
then (G ^ I) /. (i + 1) = (G ^ I) . (i + 1) by S1, PARTFUN1:def 6;
then (G ^ I) /. (i + 1) = G . (i + 1) by D3, FINSEQ_1:def 7;
hence (G ^ I) /. (i + 1) = G /. (i + 1) by D3, PARTFUN1:def 6; :: thesis: verum
end;
X2: len (G ^ I) = (len G) + (len I) by FINSEQ_1:22;
X3: for i being Element of NAT st i <= (len I) - 1 holds
(G ^ I) /. ((len G) + (i + 1)) = I /. (i + 1)
proof
let i be Element of 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 D2: i + 1 <= len I by XREAL_1:19;
1 <= i + 1 by NAT_1:11;
then D3: i + 1 in dom I by D2, FINSEQ_3:25;
D9: 1 <= (len G) + (i + 1) by NAT_1:11, XREAL_1:38;
(len G) + (i + 1) <= len (G ^ I) by X2, D2, XREAL_1:7;
then (len G) + (i + 1) in dom (G ^ I) by D9, FINSEQ_3:25;
hence (G ^ I) /. ((len G) + (i + 1)) = (G ^ I) . ((len G) + (i + 1)) by PARTFUN1:def 6
.= I . (i + 1) by D3, FINSEQ_1:def 7
.= I /. (i + 1) by D3, PARTFUN1:def 6 ;
:: thesis: verum
end;
defpred S1[ Element of NAT ] means ( $1 <= (len G) - 1 implies (PartDiffSeq (f,Z,(G ^ I))) . $1 = (PartDiffSeq (f,Z,G)) . $1 );
B1: 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 by TDef5;
hence (PartDiffSeq (f,Z,(G ^ I))) . 0 = (PartDiffSeq (f,Z,G)) . 0 by TDef5; :: thesis: verum
end;
B2: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; :: thesis: ( S1[k] implies S1[k + 1] )
assume D1: S1[k] ; :: thesis: S1[k + 1]
assume D2: k + 1 <= (len G) - 1 ; :: thesis: (PartDiffSeq (f,Z,(G ^ I))) . (k + 1) = (PartDiffSeq (f,Z,G)) . (k + 1)
D20: 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 TDef5
.= ((PartDiffSeq (f,Z,G)) . k) `partial| (Z,(G /. (k + 1))) by D20, Y0, D1, D2, XXREAL_0:2
.= (PartDiffSeq (f,Z,G)) . (k + 1) by TDef5 ; :: thesis: verum
end;
Y1: for n being Element of NAT holds S1[n] from NAT_1:sch 1(B1, B2);
 1 <= len G by FINSEQ_1:20;
then reconsider j = (len G) - 1 as Element of NAT by INT_1:5;
Y11: (PartDiffSeq (f,Z,(G ^ I))) . (len G) = ((PartDiffSeq (f,Z,(G ^ I))) . j) `partial| (Z,((G ^ I) /. (j + 1))) by TDef5
.= ((PartDiffSeq (f,Z,G)) . j) `partial| (Z,((G ^ I) /. (j + 1))) by Y1
.= ((PartDiffSeq (f,Z,G)) . j) `partial| (Z,(G /. (j + 1))) by Y0
.= (PartDiffSeq (f,Z,G)) . (len G) by TDef5 ;
defpred S2[ Element of NAT ] means ( $1 <= (len I) - 1 implies (PartDiffSeq ((f `partial| (Z,G)),Z,I)) . $1 = (PartDiffSeq (f,Z,(G ^ I))) . ((len G) + $1) );
A1: S2[ 0 ] by Y11, TDef5;
A2: for k being Element of NAT st S2[k] holds
S2[k + 1]
proof
let k be Element of NAT ; :: thesis: ( S2[k] implies S2[k + 1] )
assume A3: S2[k] ; :: thesis: S2[k + 1]
set i = (len G) + k;
assume P0: k + 1 <= (len I) - 1 ; :: thesis: (PartDiffSeq ((f `partial| (Z,G)),Z,I)) . (k + 1) = (PartDiffSeq (f,Z,(G ^ I))) . ((len G) + (k + 1))
P1: k <= k + 1 by NAT_1:11;
(G ^ I) /. (((len G) + k) + 1) = (G ^ I) /. ((len G) + (k + 1)) ;
then P2: (G ^ I) /. (((len G) + k) + 1) = I /. (k + 1) by X3, P1, P0, 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 TDef5;
hence (PartDiffSeq ((f `partial| (Z,G)),Z,I)) . (k + 1) = (PartDiffSeq (f,Z,(G ^ I))) . ((len G) + (k + 1)) by P1, P0, A3, P2, TDef5, XXREAL_0:2; :: thesis: verum
end;
X1: for n being Element of NAT holds S2[n] from NAT_1:sch 1(A1, A2);
hereby :: thesis: ( 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 )
assume P1: f is_partial_differentiable_on Z,G ^ I ; :: thesis: ( f is_partial_differentiable_on Z,G & f `partial| (Z,G) is_partial_differentiable_on Z,I )
now :: thesis: for i being Element of NAT st i <= (len G) - 1 holds
(PartDiffSeq (f,Z,G)) . i is_partial_differentiable_on Z,G /. (i + 1)
let i be Element of NAT ; :: thesis: ( i <= (len G) - 1 implies (PartDiffSeq (f,Z,G)) . i is_partial_differentiable_on Z,G /. (i + 1) )
assume D1: i <= (len G) - 1 ; :: thesis: (PartDiffSeq (f,Z,G)) . i is_partial_differentiable_on Z,G /. (i + 1)
then i + Z0 <= ((len G) - 1) + (len I) by XREAL_1:7;
then i <= (len (G ^ I)) - 1 by X2;
then P2: (PartDiffSeq (f,Z,(G ^ I))) . i is_partial_differentiable_on Z,(G ^ I) /. (i + 1) by TDef6, P1;
(G ^ I) /. (i + 1) = G /. (i + 1) by D1, Y0;
hence (PartDiffSeq (f,Z,G)) . i is_partial_differentiable_on Z,G /. (i + 1) by P2, D1, Y1; :: thesis: verum
end;
hence f is_partial_differentiable_on Z,G by TDef6; :: thesis: f `partial| (Z,G) is_partial_differentiable_on Z,I
now :: thesis: for i being Element of NAT st i <= (len I) - 1 holds
(PartDiffSeq ((f `partial| (Z,G)),Z,I)) . i is_partial_differentiable_on Z,I /. (i + 1)
let i be Element of NAT ; :: thesis: ( i <= (len I) - 1 implies (PartDiffSeq ((f `partial| (Z,G)),Z,I)) . i is_partial_differentiable_on Z,I /. (i + 1) )
assume S1: i <= (len I) - 1 ; :: thesis: (PartDiffSeq ((f `partial| (Z,G)),Z,I)) . i is_partial_differentiable_on Z,I /. (i + 1)
then (len G) + i <= (len G) + ((len I) - 1) by XREAL_1:6;
then (len G) + i <= (len (G ^ I)) - 1 by X2;
then X4: (PartDiffSeq (f,Z,(G ^ I))) . ((len G) + i) is_partial_differentiable_on Z,(G ^ I) /. (((len G) + i) + 1) by TDef6, P1;
(G ^ I) /. (((len G) + i) + 1) = (G ^ I) /. ((len G) + (i + 1)) ;
then (G ^ I) /. (((len G) + i) + 1) = I /. (i + 1) by S1, X3;
hence (PartDiffSeq ((f `partial| (Z,G)),Z,I)) . i is_partial_differentiable_on Z,I /. (i + 1) by X4, S1, X1; :: thesis: verum
end;
hence f `partial| (Z,G) is_partial_differentiable_on Z,I by TDef6; :: thesis: verum
end;
now :: thesis: ( 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 )
assume P0: ( f is_partial_differentiable_on Z,G & f `partial| (Z,G) is_partial_differentiable_on Z,I ) ; :: thesis: f is_partial_differentiable_on Z,G ^ I
now :: thesis: for i being Element of NAT st i <= (len (G ^ I)) - 1 holds
(PartDiffSeq (f,Z,(G ^ I))) . i is_partial_differentiable_on Z,(G ^ I) /. (i + 1)
let i be Element of NAT ; :: thesis: ( i <= (len (G ^ I)) - 1 implies (PartDiffSeq (f,Z,(G ^ I))) . b1 is_partial_differentiable_on Z,(G ^ I) /. (b1 + 1) )
assume Q1: i <= (len (G ^ I)) - 1 ; :: thesis: (PartDiffSeq (f,Z,(G ^ I))) . b1 is_partial_differentiable_on Z,(G ^ I) /. (b1 + 1)
per cases ( i <= (len G) - 1 or not i <= (len G) - 1 ) ;
suppose Q2: i <= (len G) - 1 ; :: thesis: (PartDiffSeq (f,Z,(G ^ I))) . b1 is_partial_differentiable_on Z,(G ^ I) /. (b1 + 1)
then Q3: (PartDiffSeq (f,Z,G)) . i is_partial_differentiable_on Z,G /. (i + 1) by TDef6, P0;
G /. (i + 1) = (G ^ I) /. (i + 1) by Q2, Y0;
hence (PartDiffSeq (f,Z,(G ^ I))) . i is_partial_differentiable_on Z,(G ^ I) /. (i + 1) by Q2, Y1, Q3; :: thesis: verum
end;
suppose not i <= (len G) - 1 ; :: thesis: (PartDiffSeq (f,Z,(G ^ I))) . b1 is_partial_differentiable_on Z,(G ^ I) /. (b1 + 1)
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;
R5: i - (len G) <= (((len G) + (len I)) - 1) - (len G) by Q1, X2, XREAL_1:9;
then Q5: ( k <= (len I) - 1 & i = k + (len G) ) ;
then Q6: (PartDiffSeq ((f `partial| (Z,G)),Z,I)) . k is_partial_differentiable_on Z,I /. (k + 1) by TDef6, P0;
i + 1 = (k + 1) + (len G) ;
then I /. (k + 1) = (G ^ I) /. (i + 1) by R5, X3;
hence (PartDiffSeq (f,Z,(G ^ I))) . i is_partial_differentiable_on Z,(G ^ I) /. (i + 1) by Q6, Q5, X1; :: thesis: verum
end;
end;
end;
hence f is_partial_differentiable_on Z,G ^ I by TDef6; :: thesis: verum
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: verum