:: ARITHM semantic presentation

theorem Th1: :: ARITHM:1

for b₁ being complex number holds b₁ + 0 = b₁

proof end;

Lemma2: - 0 = 0

proof end;

Lemma3: opp 0 = 0

proof end;

theorem Th2: :: ARITHM:2

for b₁ being complex number holds b₁ * 0 = 0

proof end;

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

theorem Th3: :: ARITHM:3

for b₁ being complex number holds 1 * b₁ = b₁

proof end;

theorem Th4: :: ARITHM:4

for b₁ being complex number holds b₁ - 0 = b₁

proof end;

theorem Th5: :: ARITHM:5

for b₁ being complex number holds 0 / b₁ = 0

proof end;

Lemma7: 1 " = 1

proof end;

theorem Th6: :: ARITHM:6

for b₁ being complex number holds b₁ / 1 = b₁

proof end;