theorem Th12: :: NDIFF14:12

for S being RealNormSpace-Sequence
for T being RealNormSpace
for I being non empty FinSequence of dom S holds
( Partdiff_SP (S,T,I,1) = R_NormSpace_of_BoundedLinearOperators ((S . (In ((I . 1),(dom S)))),T) & ( for i being Nat st 1 <= i & i < len I holds
Partdiff_SP (S,T,I,(i + 1)) = R_NormSpace_of_BoundedLinearOperators ((S . (In ((I . (i + 1)),(dom S)))),(Partdiff_SP (S,T,I,i))) ) )