let S be RealNormSpace-Sequence; :: thesis: for T being RealNormSpace
for Z being Subset of (product S)
for G being non empty FinSequence of dom S
for s being Element of dom S
for f being PartFunc of (product S),T holds
( Partdiff_SP (S,(Partdiff_SP (S,T,G,(len G))),<*s*>,1) = Partdiff_SP (S,T,(G ^ <*s*>),((len G) + 1)) & (f `partial| (Z,G)) `partial| (Z,s) = PartDiffSeq (f,Z,(G ^ <*s*>),((len G) + 1)) )
let T be RealNormSpace; :: thesis: for Z being Subset of (product S)
for G being non empty FinSequence of dom S
for s being Element of dom S
for f being PartFunc of (product S),T holds
( Partdiff_SP (S,(Partdiff_SP (S,T,G,(len G))),<*s*>,1) = Partdiff_SP (S,T,(G ^ <*s*>),((len G) + 1)) & (f `partial| (Z,G)) `partial| (Z,s) = PartDiffSeq (f,Z,(G ^ <*s*>),((len G) + 1)) )
let Z be Subset of (product S); :: thesis: for G being non empty FinSequence of dom S
for s being Element of dom S
for f being PartFunc of (product S),T holds
( Partdiff_SP (S,(Partdiff_SP (S,T,G,(len G))),<*s*>,1) = Partdiff_SP (S,T,(G ^ <*s*>),((len G) + 1)) & (f `partial| (Z,G)) `partial| (Z,s) = PartDiffSeq (f,Z,(G ^ <*s*>),((len G) + 1)) )
let G be non empty FinSequence of dom S; :: thesis: for s being Element of dom S
for f being PartFunc of (product S),T holds
( Partdiff_SP (S,(Partdiff_SP (S,T,G,(len G))),<*s*>,1) = Partdiff_SP (S,T,(G ^ <*s*>),((len G) + 1)) & (f `partial| (Z,G)) `partial| (Z,s) = PartDiffSeq (f,Z,(G ^ <*s*>),((len G) + 1)) )
let s be Element of dom S; :: thesis: for f being PartFunc of (product S),T holds
( Partdiff_SP (S,(Partdiff_SP (S,T,G,(len G))),<*s*>,1) = Partdiff_SP (S,T,(G ^ <*s*>),((len G) + 1)) & (f `partial| (Z,G)) `partial| (Z,s) = PartDiffSeq (f,Z,(G ^ <*s*>),((len G) + 1)) )
let f be PartFunc of (product S),T; :: thesis: ( Partdiff_SP (S,(Partdiff_SP (S,T,G,(len G))),<*s*>,1) = Partdiff_SP (S,T,(G ^ <*s*>),((len G) + 1)) & (f `partial| (Z,G)) `partial| (Z,s) = PartDiffSeq (f,Z,(G ^ <*s*>),((len G) + 1)) )
set I = <*s*>;
A1: len <*s*> = 1 by FINSEQ_1:39;
hence Partdiff_SP (S,(Partdiff_SP (S,T,G,(len G))),<*s*>,1) = Partdiff_SP (S,T,(G ^ <*s*>),((len G) + 1)) by Th17; :: thesis: (f `partial| (Z,G)) `partial| (Z,s) = PartDiffSeq (f,Z,(G ^ <*s*>),((len G) + 1))
PartDiffSeq ((f `partial| (Z,G)),Z,<*s*>,(len <*s*>)) = (f `partial| (Z,G)) `partial| (Z,(<*s*> . 1)) by A1, Th13
.= (f `partial| (Z,G)) `partial| (Z,s) ;
hence (f `partial| (Z,G)) `partial| (Z,s) = PartDiffSeq (f,Z,(G ^ <*s*>),((len G) + 1)) by A1, Th17; :: thesis: verum