:: deftheorem Def3 defines Partdiff_SP NDIFF14:def 3 :
for S being RealNormSpace-Sequence
for T being RealNormSpace
for I being non empty FinSequence of dom S
for b₄ being RealNormSpace-Sequence holds
( b₄ = Partdiff_SP (S,T,I) iff ( dom b₄ = dom I & b₄ . 1 = R_NormSpace_of_BoundedLinearOperators ((S . (In ((I . 1),(dom S)))),T) & ( for i being Nat st 1 <= i & i < len I holds
b₄ . (i + 1) = R_NormSpace_of_BoundedLinearOperators ((S . (In ((I . (i + 1)),(dom S)))),(modetrans (b₄ . i))) ) ) );