for x being Complex holds x + 0 = x