theorem Th3: :: ARITHM:3

for x being Complex holds 1 * x = x