theorem Th53: :: CLVECT_3:53

for X being ComplexUnitarySpace
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)