for X being Banach_Algebra
for z being Element of X
for seq being sequence of X holds
( Partial_Sums (z * seq) = z * (Partial_Sums seq) & Partial_Sums (seq * z) = (Partial_Sums seq) * z )