let X be ComplexUnitarySpace; :: thesis: for seq being sequence of X
for Cseq being Complex_Sequence
for n being Element of 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 Element of 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 Element of 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 Element of 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:43;
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:28;
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:26;
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:14;
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:14;
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:21;
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 15;
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:4; :: thesis: verum