theorem Th16:
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
( ( for
n being
Nat st 1
<= n &
n <= len G holds
(
Partdiff_SP (
S,
T,
(G ^ I),
n)
= Partdiff_SP (
S,
T,
G,
n) &
PartDiffSeq (
f,
Z,
(G ^ I),
n)
= PartDiffSeq (
f,
Z,
G,
n) ) ) & ( for
n being
Nat st 1
<= n &
n <= len I holds
(
Partdiff_SP (
S,
(Partdiff_SP (S,T,G,(len G))),
I,
n)
= Partdiff_SP (
S,
T,
(G ^ I),
((len G) + n)) &
PartDiffSeq (
(f `partial| (Z,G)),
Z,
I,
n)
= PartDiffSeq (
f,
Z,
(G ^ I),
((len G) + n)) ) ) )