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
( 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)) & Partdiff_SP (S,(Partdiff_SP (S,T,G,(len G))),I,(len I)) = Partdiff_SP (S,T,(G ^ I),((len G) + (len I))) & PartDiffSeq ((f `partial| (Z,G)),Z,I,(len I)) = PartDiffSeq (f,Z,(G ^ I),((len G) + (len I))) )
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
( 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)) & Partdiff_SP (S,(Partdiff_SP (S,T,G,(len G))),I,(len I)) = Partdiff_SP (S,T,(G ^ I),((len G) + (len I))) & PartDiffSeq ((f `partial| (Z,G)),Z,I,(len I)) = PartDiffSeq (f,Z,(G ^ I),((len G) + (len I))) )
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
( 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)) & Partdiff_SP (S,(Partdiff_SP (S,T,G,(len G))),I,(len I)) = Partdiff_SP (S,T,(G ^ I),((len G) + (len I))) & PartDiffSeq ((f `partial| (Z,G)),Z,I,(len I)) = PartDiffSeq (f,Z,(G ^ I),((len G) + (len I))) )
let I, G be non empty FinSequence of dom S; :: thesis: for f being PartFunc of (product S),T holds
( 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)) & Partdiff_SP (S,(Partdiff_SP (S,T,G,(len G))),I,(len I)) = Partdiff_SP (S,T,(G ^ I),((len G) + (len I))) & PartDiffSeq ((f `partial| (Z,G)),Z,I,(len I)) = PartDiffSeq (f,Z,(G ^ I),((len G) + (len I))) )
let f be PartFunc of (product S),T; :: thesis: ( 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)) & Partdiff_SP (S,(Partdiff_SP (S,T,G,(len G))),I,(len I)) = Partdiff_SP (S,T,(G ^ I),((len G) + (len I))) & PartDiffSeq ((f `partial| (Z,G)),Z,I,(len I)) = PartDiffSeq (f,Z,(G ^ I),((len G) + (len I))) )
1 <= len G by FINSEQ_1:20;
hence ( 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 Th16; :: thesis: ( Partdiff_SP (S,(Partdiff_SP (S,T,G,(len G))),I,(len I)) = Partdiff_SP (S,T,(G ^ I),((len G) + (len I))) & PartDiffSeq ((f `partial| (Z,G)),Z,I,(len I)) = PartDiffSeq (f,Z,(G ^ I),((len G) + (len I))) )
1 <= len I by FINSEQ_1:20;
hence ( Partdiff_SP (S,(Partdiff_SP (S,T,G,(len G))),I,(len I)) = Partdiff_SP (S,T,(G ^ I),((len G) + (len I))) & PartDiffSeq ((f `partial| (Z,G)),Z,I,(len I)) = PartDiffSeq (f,Z,(G ^ I),((len G) + (len I))) ) by Th16; :: thesis: verum