for x being Complex holds 1 * x = x