begin
theorem
canceled;
theorem
canceled;
:: deftheorem Def1 defines F_Complex COMPLFLD:def 1 :
for b1 being strict doubleLoopStr holds
( b1 = F_Complex iff ( the carrier of b1 = COMPLEX & the addF of b1 = addcomplex & the multF of b1 = multcomplex & 1. b1 = 1r & 0. b1 = 0c ) );
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
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
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 :
for x being Element of F_Complex
for n being non empty Element of NAT
for b3 being Element of F_Complex holds
( b3 is CRoot of n,x iff (power F_Complex) . (b3,n) = x );
theorem
theorem
theorem