theorem Th1: :: ARITHM:1

for x being Complex holds x + 0 = x