theorem :: BHSP_4:5

for a, b being Real
for X being RealUnitarySpace
for seq1, seq2 being sequence of X holds (a * (Partial_Sums seq1)) + (b * (Partial_Sums seq2)) = Partial_Sums ((a * seq1) + (b * seq2))