begin
theorem
canceled;
theorem
canceled;
:: deftheorem Def1 defines F_Complex COMPLFLD:def 1 :
Lm1:
1_ F_Complex = 1r
by Def1;
Lm2:
1. F_Complex = 1r
by Def1;
theorem
theorem Th4:
theorem Th5:
theorem
theorem Th7:
theorem Th8:
theorem Th9:
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
for
z1,
z2 being
Element of holds
z1 - (- z2) = z1 + z2
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
for
z1,
z being
Element of holds
z1 = (z1 + z) - z
theorem
for
z1,
z being
Element of holds
z1 = (z1 - z) + z
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
theorem
canceled;
theorem
theorem
canceled;
theorem
theorem
theorem
canceled;
theorem
theorem
theorem
theorem
theorem Th62:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th84:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
canceled;
theorem
theorem
theorem
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
begin
theorem Th112:
:: deftheorem Def2 defines CRoot COMPLFLD:def 2 :
theorem
theorem
theorem