theorem Th52: :: BHSP_4:52

for Rseq being Real_Sequence
for X being RealUnitarySpace
for seq being sequence of X
for n being Nat holds (Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . n = ((Partial_Sums (Rseq * seq)) . (n + 1)) - ((Rseq * (Partial_Sums seq)) . (n + 1))