theorem Th53: :: BHSP_4:53

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