theorem
for
S being
RealNormSpace-Sequence 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)) )