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