:: ARITHM semantic presentation

theorem Th1: :: ARITHM:1

for x being complex number holds x + 0 = x

proof end;

Lm1: - 0 = 0

proof end;

Lm2: opp 0 = 0

proof end;

theorem Th2: :: ARITHM:2

for x being complex number holds x * 0 = 0

proof end;

Lm3: one = succ 0 by ORDINAL2:def 4
.= 1 ;

theorem Th3: :: ARITHM:3

for x being complex number holds 1 * x = x

proof end;

theorem :: ARITHM:4

for x being complex number holds x - 0 = x

proof end;

theorem :: ARITHM:5

for x being complex number holds 0 / x = 0

proof end;

Lm4: 1 " = 1

proof end;

theorem :: ARITHM:6

for x being complex number holds x / 1 = x

proof end;