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