theorem Th52: :: CLVECT_3:52

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