begin
Lm1:
for a, b being complex number holds (a ") * (b ") = (a * b) "
Lm2:
for a, b, c being complex number holds a / (b / c) = (a * c) / b
Lm3:
for b, a being complex number st b <> 0 holds
(a / b) * b = a
Lm4:
for a being complex number holds 1 / a = a "
Lm5:
for a being complex number st a <> 0 holds
a / a = 1
Lm6:
for a, b, c, d being complex number holds (a / b) * (c / d) = (a * c) / (b * d)
Lm7:
for a, b being complex number holds (a / b) " = b / a
Lm8:
for a, b, c being complex number holds a * (b / c) = (a * b) / c
Lm9:
for b, a being complex number st b <> 0 holds
a = (a * b) / b
Lm10:
for c, a, b being complex number st c <> 0 holds
a / b = (a * c) / (b * c)
Lm11:
for a, b being complex number holds (a * (b ")) " = (a ") * b
Lm12:
for a, b being complex number st a " = b " holds
a = b
Lm13:
for a, b, c, d being complex number holds (a / b) / (c / d) = (a * d) / (b * c)
Lm14:
for a, b being complex number holds a * (1 / b) = a / b
Lm15:
for c, a, b being complex number holds (1 / c) * (a / b) = a / (b * c)
Lm16:
for a being complex number holds 1 / (a ") = a
Lm17:
for a, b being complex number holds - (a / b) = (- a) / b
Lm18:
for a being complex number st a <> 0 & a = a " & not a = 1 holds
a = - 1
Lm19:
for a being complex number holds (- a) " = - (a ")
begin
begin