for X being non empty right_complementable add-associative right_zeroed CNORMSTR
for seq being sequence of X st ( for n being Nat holds seq . n = 0. X ) holds
for m being Nat holds (Partial_Sums seq) . m = 0. X