let Rseq be Real_Sequence; :: thesis: for X being RealUnitarySpace
for seq being sequence of X
for n being Nat holds (Partial_Sums (Rseq * seq)) . (n + 1) = ((Rseq * (Partial_Sums seq)) . (n + 1)) - ((Partial_Sums (((Rseq ^\ 1) - Rseq) * (Partial_Sums seq))) . n)
let X be RealUnitarySpace; :: thesis: for seq being sequence of X
for n being Nat holds (Partial_Sums (Rseq * seq)) . (n + 1) = ((Rseq * (Partial_Sums seq)) . (n + 1)) - ((Partial_Sums (((Rseq ^\ 1) - Rseq) * (Partial_Sums seq))) . n)
let seq be sequence of X; :: thesis: for n being Nat holds (Partial_Sums (Rseq * seq)) . (n + 1) = ((Rseq * (Partial_Sums seq)) . (n + 1)) - ((Partial_Sums (((Rseq ^\ 1) - Rseq) * (Partial_Sums seq))) . n)
let n be Nat; :: thesis: (Partial_Sums (Rseq * seq)) . (n + 1) = ((Rseq * (Partial_Sums seq)) . (n + 1)) - ((Partial_Sums (((Rseq ^\ 1) - Rseq) * (Partial_Sums seq))) . n)
((Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . n) + ((Rseq * (Partial_Sums seq)) . (n + 1)) = (((Partial_Sums (Rseq * seq)) . (n + 1)) - ((Rseq * (Partial_Sums seq)) . (n + 1))) + ((Rseq * (Partial_Sums seq)) . (n + 1)) by Th52;
then ((Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . n) + ((Rseq * (Partial_Sums seq)) . (n + 1)) = ((Partial_Sums (Rseq * seq)) . (n + 1)) - (((Rseq * (Partial_Sums seq)) . (n + 1)) - ((Rseq * (Partial_Sums seq)) . (n + 1))) by RLVECT_1:29;
then ((Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . n) + ((Rseq * (Partial_Sums seq)) . (n + 1)) = ((Partial_Sums (Rseq * seq)) . (n + 1)) - H₁(X) by RLVECT_1:15;
then (Partial_Sums (Rseq * seq)) . (n + 1) = ((Rseq * (Partial_Sums seq)) . (n + 1)) + ((Partial_Sums ((((- 1) (#) (Rseq ^\ 1)) - (- Rseq)) * (Partial_Sums seq))) . n) ;
then (Partial_Sums (Rseq * seq)) . (n + 1) = ((Rseq * (Partial_Sums seq)) . (n + 1)) + ((Partial_Sums (((- 1) (#) ((Rseq ^\ 1) - Rseq)) * (Partial_Sums seq))) . n) by SEQ_1:24;
then (Partial_Sums (Rseq * seq)) . (n + 1) = ((Rseq * (Partial_Sums seq)) . (n + 1)) + ((Partial_Sums ((- 1) * (((Rseq ^\ 1) - Rseq) * (Partial_Sums seq)))) . n) by Th46;
then (Partial_Sums (Rseq * seq)) . (n + 1) = ((Rseq * (Partial_Sums seq)) . (n + 1)) + (((- 1) * (Partial_Sums (((Rseq ^\ 1) - Rseq) * (Partial_Sums seq)))) . n) by Th3;
then (Partial_Sums (Rseq * seq)) . (n + 1) = ((Rseq * (Partial_Sums seq)) . (n + 1)) + ((- 1) * ((Partial_Sums (((Rseq ^\ 1) - Rseq) * (Partial_Sums seq))) . n)) by NORMSP_1:def 5;
hence (Partial_Sums (Rseq * seq)) . (n + 1) = ((Rseq * (Partial_Sums seq)) . (n + 1)) - ((Partial_Sums (((Rseq ^\ 1) - Rseq) * (Partial_Sums seq))) . n) by RLVECT_1:16; :: thesis: verum