theorem Th15: :: CLOPBAN4:15
for X being Complex_Banach_Algebra
for k being Nat
for seq being sequence of X holds (Partial_Sums seq) . k = ((Partial_Sums (Shift seq)) . k) + (seq . k)