for V being non empty right_complementable Abelian add-associative right_zeroed CLSStruct holds Sum (ZeroCLC V) = 0. V