for X being ComplexUnitarySpace
for seq being sequence of X
for Cseq being Complex_Sequence
for n being Nat holds Sum ((Cseq * seq),(n + 1)) = ((Cseq * (Partial_Sums seq)) . (n + 1)) - (Sum ((((Cseq ^\ 1) - Cseq) * (Partial_Sums seq)),n)) by Th53;