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