let S be RealNormSpace-Sequence; :: thesis: 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))) ) )
let T be RealNormSpace; :: thesis: 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))) ) )
let I be non empty FinSequence of dom S; :: thesis: ( 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))) ) )
1 <= len I by FINSEQ_1:20;
hence Partdiff_SP (S,T,I,1) = (Partdiff_SP (S,T,I)) . 1 by Def4
.= R_NormSpace_of_BoundedLinearOperators ((S . (In ((I . 1),(dom S)))),T) by Def3 ;
:: thesis: 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)))
let i be Nat; :: thesis: ( 1 <= i & i < len I implies Partdiff_SP (S,T,I,(i + 1)) = R_NormSpace_of_BoundedLinearOperators ((S . (In ((I . (i + 1)),(dom S)))),(Partdiff_SP (S,T,I,i))) )
assume A1: ( 1 <= i & i < len I ) ; :: thesis: Partdiff_SP (S,T,I,(i + 1)) = R_NormSpace_of_BoundedLinearOperators ((S . (In ((I . (i + 1)),(dom S)))),(Partdiff_SP (S,T,I,i)))
then A2: ( 1 <= i + 1 & i + 1 <= len I ) by NAT_1:13;
A3: Partdiff_SP (S,T,I,i) = (Partdiff_SP (S,T,I)) . i by A1, Def4;
thus Partdiff_SP (S,T,I,(i + 1)) = (Partdiff_SP (S,T,I)) . (i + 1) by A2, Def4
.= R_NormSpace_of_BoundedLinearOperators ((S . (In ((I . (i + 1)),(dom S)))),(modetrans ((Partdiff_SP (S,T,I)) . i))) by A1, Def3
.= R_NormSpace_of_BoundedLinearOperators ((S . (In ((I . (i + 1)),(dom S)))),(Partdiff_SP (S,T,I,i))) by A3, NDIFF_6:def 1 ; :: thesis: verum