let S be RealNormSpace-Sequence; :: thesis: for T being RealNormSpace
for Z being Subset of (product S)
for I, G being non empty FinSequence of dom S
for f being PartFunc of (product S),T holds
( ( for n being Nat st 1 <= n & n <= len G holds
( Partdiff_SP (S,T,(G ^ I),n) = Partdiff_SP (S,T,G,n) & PartDiffSeq (f,Z,(G ^ I),n) = PartDiffSeq (f,Z,G,n) ) ) & ( for n being Nat st 1 <= n & n <= len I holds
( Partdiff_SP (S,(Partdiff_SP (S,T,G,(len G))),I,n) = Partdiff_SP (S,T,(G ^ I),((len G) + n)) & PartDiffSeq ((f `partial| (Z,G)),Z,I,n) = PartDiffSeq (f,Z,(G ^ I),((len G) + n)) ) ) )
let T be RealNormSpace; :: thesis: for Z being Subset of (product S)
for I, G being non empty FinSequence of dom S
for f being PartFunc of (product S),T holds
( ( for n being Nat st 1 <= n & n <= len G holds
( Partdiff_SP (S,T,(G ^ I),n) = Partdiff_SP (S,T,G,n) & PartDiffSeq (f,Z,(G ^ I),n) = PartDiffSeq (f,Z,G,n) ) ) & ( for n being Nat st 1 <= n & n <= len I holds
( Partdiff_SP (S,(Partdiff_SP (S,T,G,(len G))),I,n) = Partdiff_SP (S,T,(G ^ I),((len G) + n)) & PartDiffSeq ((f `partial| (Z,G)),Z,I,n) = PartDiffSeq (f,Z,(G ^ I),((len G) + n)) ) ) )
let Z be Subset of (product S); :: thesis: for I, G being non empty FinSequence of dom S
for f being PartFunc of (product S),T holds
( ( for n being Nat st 1 <= n & n <= len G holds
( Partdiff_SP (S,T,(G ^ I),n) = Partdiff_SP (S,T,G,n) & PartDiffSeq (f,Z,(G ^ I),n) = PartDiffSeq (f,Z,G,n) ) ) & ( for n being Nat st 1 <= n & n <= len I holds
( Partdiff_SP (S,(Partdiff_SP (S,T,G,(len G))),I,n) = Partdiff_SP (S,T,(G ^ I),((len G) + n)) & PartDiffSeq ((f `partial| (Z,G)),Z,I,n) = PartDiffSeq (f,Z,(G ^ I),((len G) + n)) ) ) )
let I, G be non empty FinSequence of dom S; :: thesis: for f being PartFunc of (product S),T holds
( ( for n being Nat st 1 <= n & n <= len G holds
( Partdiff_SP (S,T,(G ^ I),n) = Partdiff_SP (S,T,G,n) & PartDiffSeq (f,Z,(G ^ I),n) = PartDiffSeq (f,Z,G,n) ) ) & ( for n being Nat st 1 <= n & n <= len I holds
( Partdiff_SP (S,(Partdiff_SP (S,T,G,(len G))),I,n) = Partdiff_SP (S,T,(G ^ I),((len G) + n)) & PartDiffSeq ((f `partial| (Z,G)),Z,I,n) = PartDiffSeq (f,Z,(G ^ I),((len G) + n)) ) ) )
let f be PartFunc of (product S),T; :: thesis: ( ( for n being Nat st 1 <= n & n <= len G holds
( Partdiff_SP (S,T,(G ^ I),n) = Partdiff_SP (S,T,G,n) & PartDiffSeq (f,Z,(G ^ I),n) = PartDiffSeq (f,Z,G,n) ) ) & ( for n being Nat st 1 <= n & n <= len I holds
( Partdiff_SP (S,(Partdiff_SP (S,T,G,(len G))),I,n) = Partdiff_SP (S,T,(G ^ I),((len G) + n)) & PartDiffSeq ((f `partial| (Z,G)),Z,I,n) = PartDiffSeq (f,Z,(G ^ I),((len G) + n)) ) ) )
A1: for i being Nat st i < len G holds
(G ^ I) . (i + 1) = G . (i + 1)
proof
let i be Nat; :: thesis: ( i < len G implies (G ^ I) . (i + 1) = G . (i + 1) )
assume i < len G ; :: thesis: (G ^ I) . (i + 1) = G . (i + 1)
then ( 1 <= i + 1 & i + 1 <= len G ) by NAT_1:11, NAT_1:13;
then i + 1 in dom G by FINSEQ_3:25;
hence (G ^ I) . (i + 1) = G . (i + 1) by FINSEQ_1:def 7; :: thesis: verum
end;
A2: for i being Nat st i < len I holds
(G ^ I) . ((len G) + (i + 1)) = I . (i + 1)
proof
let i be Nat; :: thesis: ( i < len I implies (G ^ I) . ((len G) + (i + 1)) = I . (i + 1) )
assume i < len I ; :: thesis: (G ^ I) . ((len G) + (i + 1)) = I . (i + 1)
then i + 1 <= len I by NAT_1:13;
then A3: i + 1 in dom I by NAT_1:11, FINSEQ_3:25;
thus (G ^ I) . ((len G) + (i + 1)) = I . (i + 1) by A3, FINSEQ_1:def 7; :: thesis: verum
end;
defpred S1[ Nat] means ( 1 <= $1 & $1 <= len G implies ( Partdiff_SP (S,T,(G ^ I),$1) = Partdiff_SP (S,T,G,$1) & PartDiffSeq (f,Z,(G ^ I),$1) = PartDiffSeq (f,Z,G,$1) ) );
A4: S1[ 0 ] ;
A5: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A6: S1[k] ; :: thesis: S1[k + 1]
assume A7: ( 1 <= k + 1 & k + 1 <= len G ) ; :: thesis: ( Partdiff_SP (S,T,(G ^ I),(k + 1)) = Partdiff_SP (S,T,G,(k + 1)) & PartDiffSeq (f,Z,(G ^ I),(k + 1)) = PartDiffSeq (f,Z,G,(k + 1)) )
k < k + 1 by NAT_1:19;
then A8: k < len G by A7, XXREAL_0:2;
per cases ( k = 0 or k <> 0 ) ;
suppose A9: k = 0 ; :: thesis: ( Partdiff_SP (S,T,(G ^ I),(k + 1)) = Partdiff_SP (S,T,G,(k + 1)) & PartDiffSeq (f,Z,(G ^ I),(k + 1)) = PartDiffSeq (f,Z,G,(k + 1)) )
hence Partdiff_SP (S,T,(G ^ I),(k + 1)) = R_NormSpace_of_BoundedLinearOperators ((S . (In (((G ^ I) . (k + 1)),(dom S)))),T) by Th12
.= R_NormSpace_of_BoundedLinearOperators ((S . (In ((G . (k + 1)),(dom S)))),T) by A8, A1
.= Partdiff_SP (S,T,G,(k + 1)) by A9, Th12 ;
:: thesis: PartDiffSeq (f,Z,(G ^ I),(k + 1)) = PartDiffSeq (f,Z,G,(k + 1))
thus PartDiffSeq (f,Z,(G ^ I),(k + 1)) = f `partial| (Z,((G ^ I) . (k + 1))) by Th13, A9
.= f `partial| (Z,(G . (k + 1))) by A8, A1
.= PartDiffSeq (f,Z,G,(k + 1)) by Th13, A9 ; :: thesis: verum
end;
suppose A10: k <> 0 ; :: thesis: ( Partdiff_SP (S,T,(G ^ I),(k + 1)) = Partdiff_SP (S,T,G,(k + 1)) & PartDiffSeq (f,Z,(G ^ I),(k + 1)) = PartDiffSeq (f,Z,G,(k + 1)) )
len (G ^ I) = (len G) + (len I) by FINSEQ_1:22;
then len G <= len (G ^ I) by NAT_1:11;
then A11: ( 1 <= k & k < len (G ^ I) ) by A8, A10, NAT_1:14, XXREAL_0:2;
hence Partdiff_SP (S,T,(G ^ I),(k + 1)) = R_NormSpace_of_BoundedLinearOperators ((S . (In (((G ^ I) . (k + 1)),(dom S)))),(Partdiff_SP (S,T,(G ^ I),k))) by Th12
.= R_NormSpace_of_BoundedLinearOperators ((S . (In ((G . (k + 1)),(dom S)))),(Partdiff_SP (S,T,G,k))) by A1, A6, A8, A10, NAT_1:14
.= Partdiff_SP (S,T,G,(k + 1)) by A8, A10, Th12, NAT_1:14 ;
:: thesis: PartDiffSeq (f,Z,(G ^ I),(k + 1)) = PartDiffSeq (f,Z,G,(k + 1))
thus PartDiffSeq (f,Z,(G ^ I),(k + 1)) = (PartDiffSeq (f,Z,(G ^ I),k)) `partial| (Z,((G ^ I) . (k + 1))) by A11, Th13
.= (PartDiffSeq (f,Z,G,k)) `partial| (Z,(G . (k + 1))) by A1, A6, A8, A10, NAT_1:14
.= PartDiffSeq (f,Z,G,(k + 1)) by A8, A10, Th13, NAT_1:14 ; :: thesis: verum
end;
end;
end;
A12: for n being Nat holds S1[n] from NAT_1:sch 2(A4, A5);
 hence for n being Nat st 1 <= n & n <= len G holds
( Partdiff_SP (S,T,(G ^ I),n) = Partdiff_SP (S,T,G,n) & PartDiffSeq (f,Z,(G ^ I),n) = PartDiffSeq (f,Z,G,n) ) ; :: thesis: for n being Nat st 1 <= n & n <= len I holds
( Partdiff_SP (S,(Partdiff_SP (S,T,G,(len G))),I,n) = Partdiff_SP (S,T,(G ^ I),((len G) + n)) & PartDiffSeq ((f `partial| (Z,G)),Z,I,n) = PartDiffSeq (f,Z,(G ^ I),((len G) + n)) )
1 <= len G by FINSEQ_1:20;
then A13: ( Partdiff_SP (S,T,(G ^ I),(len G)) = Partdiff_SP (S,T,G,(len G)) & PartDiffSeq (f,Z,(G ^ I),(len G)) = PartDiffSeq (f,Z,G,(len G)) ) by A12;
defpred S2[ Nat] means ( 1 <= $1 & $1 <= len I implies ( Partdiff_SP (S,T,(G ^ I),((len G) + $1)) = Partdiff_SP (S,(Partdiff_SP (S,T,G,(len G))),I,$1) & PartDiffSeq (f,Z,(G ^ I),((len G) + $1)) = PartDiffSeq ((f `partial| (Z,G)),Z,I,$1) ) );
A14: S2[ 0 ] ;
A15: for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
assume A16: S2[k] ; :: thesis: S2[k + 1]
set i = (len G) + k;
assume A17: ( 1 <= k + 1 & k + 1 <= len I ) ; :: thesis: ( Partdiff_SP (S,T,(G ^ I),((len G) + (k + 1))) = Partdiff_SP (S,(Partdiff_SP (S,T,G,(len G))),I,(k + 1)) & PartDiffSeq (f,Z,(G ^ I),((len G) + (k + 1))) = PartDiffSeq ((f `partial| (Z,G)),Z,I,(k + 1)) )
per cases ( k = 0 or k <> 0 ) ;
suppose A18: k = 0 ; :: thesis: ( Partdiff_SP (S,T,(G ^ I),((len G) + (k + 1))) = Partdiff_SP (S,(Partdiff_SP (S,T,G,(len G))),I,(k + 1)) & PartDiffSeq (f,Z,(G ^ I),((len G) + (k + 1))) = PartDiffSeq ((f `partial| (Z,G)),Z,I,(k + 1)) )
set i = len G;
A19: ( 1 <= len G & 1 <= len I ) by FINSEQ_1:20;
0 + (len G) < (len I) + (len G) by XREAL_1:8;
then A20: ( 1 <= len G & len G < len (G ^ I) ) by FINSEQ_1:20, FINSEQ_1:22;
1 in dom I by A19, FINSEQ_3:25;
then A21: (G ^ I) . ((len G) + 1) = I . 1 by FINSEQ_1:def 7;
thus Partdiff_SP (S,T,(G ^ I),((len G) + (k + 1))) = R_NormSpace_of_BoundedLinearOperators ((S . (In (((G ^ I) . ((len G) + 1)),(dom S)))),(Partdiff_SP (S,T,(G ^ I),(len G)))) by A18, A20, Th12
.= Partdiff_SP (S,(Partdiff_SP (S,T,G,(len G))),I,(k + 1)) by A13, A18, A21, Th12 ; :: thesis: PartDiffSeq (f,Z,(G ^ I),((len G) + (k + 1))) = PartDiffSeq ((f `partial| (Z,G)),Z,I,(k + 1))
thus PartDiffSeq (f,Z,(G ^ I),((len G) + (k + 1))) = (PartDiffSeq (f,Z,(G ^ I),(len G))) `partial| (Z,((G ^ I) . ((len G) + 1))) by A18, A20, Th13
.= PartDiffSeq ((f `partial| (Z,G)),Z,I,(k + 1)) by A13, A18, A21, Th13 ; :: thesis: verum
end;
suppose A22: k <> 0 ; :: thesis: ( Partdiff_SP (S,T,(G ^ I),((len G) + (k + 1))) = Partdiff_SP (S,(Partdiff_SP (S,T,G,(len G))),I,(k + 1)) & PartDiffSeq (f,Z,(G ^ I),((len G) + (k + 1))) = PartDiffSeq ((f `partial| (Z,G)),Z,I,(k + 1)) )
k < k + 1 by NAT_1:19;
then A23: k < len I by A17, XXREAL_0:2;
A24: (G ^ I) . (((len G) + k) + 1) = (G ^ I) . ((len G) + (k + 1))
.= I . (k + 1) by A2, A23 ;
len (G ^ I) = (len G) + (len I) by FINSEQ_1:22;
then A27: ( 1 <= (len G) + k & (len G) + k < len (G ^ I) ) by A23, NAT_1:14, XREAL_1:8;
hence Partdiff_SP (S,T,(G ^ I),((len G) + (k + 1))) = R_NormSpace_of_BoundedLinearOperators ((S . (In (((G ^ I) . (((len G) + k) + 1)),(dom S)))),(Partdiff_SP (S,T,(G ^ I),((len G) + k)))) by Th12
.= Partdiff_SP (S,(Partdiff_SP (S,T,G,(len G))),I,(k + 1)) by A16, A22, A23, A24, Th12, NAT_1:14 ;
:: thesis: PartDiffSeq (f,Z,(G ^ I),((len G) + (k + 1))) = PartDiffSeq ((f `partial| (Z,G)),Z,I,(k + 1))
thus 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 Th13, A27
.= PartDiffSeq ((f `partial| (Z,G)),Z,I,(k + 1)) by A16, A22, A23, A24, Th13, NAT_1:14 ; :: thesis: verum
end;
end;
end;
for n being Nat holds S2[n] from NAT_1:sch 2(A14, A15);
 hence for n being Nat st 1 <= n & n <= len I holds
( Partdiff_SP (S,(Partdiff_SP (S,T,G,(len G))),I,n) = Partdiff_SP (S,T,(G ^ I),((len G) + n)) & PartDiffSeq ((f `partial| (Z,G)),Z,I,n) = PartDiffSeq (f,Z,(G ^ I),((len G) + n)) ) ; :: thesis: verum