let X be ComplexUnitarySpace; :: thesis: for seq being sequence of X
for Cseq being Complex_Sequence
for n being Nat holds (Partial_Sums (Cseq * seq)) . (n + 1) = ((Cseq * (Partial_Sums seq)) . (n + 1)) - ((Partial_Sums (((Cseq ^\ 1) - Cseq) * (Partial_Sums seq))) . n)
let seq be sequence of X; :: thesis: for Cseq being Complex_Sequence
for n being Nat holds (Partial_Sums (Cseq * seq)) . (n + 1) = ((Cseq * (Partial_Sums seq)) . (n + 1)) - ((Partial_Sums (((Cseq ^\ 1) - Cseq) * (Partial_Sums seq))) . n)
let Cseq be Complex_Sequence; :: thesis: for n being Nat holds (Partial_Sums (Cseq * seq)) . (n + 1) = ((Cseq * (Partial_Sums seq)) . (n + 1)) - ((Partial_Sums (((Cseq ^\ 1) - Cseq) * (Partial_Sums seq))) . n)
let n be Nat; :: thesis: (Partial_Sums (Cseq * seq)) . (n + 1) = ((Cseq * (Partial_Sums seq)) . (n + 1)) - ((Partial_Sums (((Cseq ^\ 1) - Cseq) * (Partial_Sums seq))) . n)
((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n) + ((Cseq * (Partial_Sums seq)) . (n + 1)) = (((Partial_Sums (Cseq * seq)) . (n + 1)) - ((Cseq * (Partial_Sums seq)) . (n + 1))) + ((Cseq * (Partial_Sums seq)) . (n + 1)) by Th52;
then ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n) + ((Cseq * (Partial_Sums seq)) . (n + 1)) = ((Partial_Sums (Cseq * seq)) . (n + 1)) - (((Cseq * (Partial_Sums seq)) . (n + 1)) - ((Cseq * (Partial_Sums seq)) . (n + 1))) by RLVECT_1:29;
then ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n) + ((Cseq * (Partial_Sums seq)) . (n + 1)) = ((Partial_Sums (Cseq * seq)) . (n + 1)) - H₁(X) by RLVECT_1:15;
then (Partial_Sums (Cseq * seq)) . (n + 1) = ((Cseq * (Partial_Sums seq)) . (n + 1)) + ((Partial_Sums ((Cseq + (- (Cseq ^\ 1))) * (Partial_Sums seq))) . n) by RLVECT_1:13;
then (Partial_Sums (Cseq * seq)) . (n + 1) = ((Cseq * (Partial_Sums seq)) . (n + 1)) + ((Partial_Sums ((((- 1r) (#) (Cseq ^\ 1)) - (- Cseq)) * (Partial_Sums seq))) . n) by COMSEQ_1:11;
then (Partial_Sums (Cseq * seq)) . (n + 1) = ((Cseq * (Partial_Sums seq)) . (n + 1)) + ((Partial_Sums ((((- 1r) (#) (Cseq ^\ 1)) - ((- 1r) (#) Cseq)) * (Partial_Sums seq))) . n) by COMSEQ_1:11;
then (Partial_Sums (Cseq * seq)) . (n + 1) = ((Cseq * (Partial_Sums seq)) . (n + 1)) + ((Partial_Sums (((- 1r) (#) ((Cseq ^\ 1) - Cseq)) * (Partial_Sums seq))) . n) by COMSEQ_1:18;
then (Partial_Sums (Cseq * seq)) . (n + 1) = ((Cseq * (Partial_Sums seq)) . (n + 1)) + ((Partial_Sums ((- 1r) * (((Cseq ^\ 1) - Cseq) * (Partial_Sums seq)))) . n) by Th46;
then (Partial_Sums (Cseq * seq)) . (n + 1) = ((Cseq * (Partial_Sums seq)) . (n + 1)) + (((- 1r) * (Partial_Sums (((Cseq ^\ 1) - Cseq) * (Partial_Sums seq)))) . n) by Th3;
then (Partial_Sums (Cseq * seq)) . (n + 1) = ((Cseq * (Partial_Sums seq)) . (n + 1)) + ((- 1r) * ((Partial_Sums (((Cseq ^\ 1) - Cseq) * (Partial_Sums seq))) . n)) by CLVECT_1:def 14;
hence (Partial_Sums (Cseq * seq)) . (n + 1) = ((Cseq * (Partial_Sums seq)) . (n + 1)) - ((Partial_Sums (((Cseq ^\ 1) - Cseq) * (Partial_Sums seq))) . n) by CLVECT_1:3; :: thesis: verum