set F = F_Complex ;
set p = X^2+X+1 ;
set M = {zeta,(zeta ^2)};
F_Real is Subfield of F_Complex by FIELD_4:7;
then the carrier of F_Real c= the carrier of F_Complex by EC_PF_1:def 1;
then reconsider r = 3-Root(2) as Element of F_Complex ;
reconsider z = zeta as Complex ;
H: Roots (F_Complex,X^2+X+1) = { a where a is Element of F_Complex : a is_a_root_of X^2+X+1 , F_Complex } by FIELD_4:def 4;
K: zeta |^ 2 = zeta * zeta by lemI;
K1: (zeta ^2) |^ 2 = (zeta ^2) |^ (1 + 1)
.= ((zeta ^2) |^ 1) * ((zeta ^2) |^ 1) by BINOM:10
.= ((zeta ^2) |^ 1) * (zeta ^2) by BINOM:8
.= (zeta ^2) * (zeta ^2) by BINOM:8 ;
zeta = (- (1 / 2)) + (<i> * ((sqrt 3) / 2)) ;
then D1: ( Re zeta = - (1 / 2) & Im zeta = (sqrt 3) / 2 ) by COMPLEX1:12;
then D2: Re (zeta * zeta) = ((- (1 / 2)) ^2) - (((sqrt 3) / 2) ^2) by COMPLEX1:16
.= ((- (1 / 2)) ^2) - (((sqrt 3) / 2) * ((sqrt 3) / 2)) by SQUARE_1:def 1
.= ((- (1 / 2)) ^2) - (((sqrt 3) * (sqrt 3)) / (2 * 2))
.= ((- (1 / 2)) ^2) - (((sqrt 3) ^2) / (2 * 2)) by SQUARE_1:def 1
.= ((- (1 / 2)) ^2) - (3 / (2 * 2)) by SQUARE_1:def 2
.= ((- (1 / 2)) * (- (1 / 2))) - (3 / (2 * 2)) by SQUARE_1:def 1
.= - (1 / 2) ;
D3: Im (zeta * zeta) = 2 * ((- (1 / 2)) * ((sqrt 3) / 2)) by D1, COMPLEX1:16
.= - ((sqrt 3) / 2) ;

now :: thesis: for o being object st o in {zeta,(zeta ^2)} holds
o in Roots (F_Complex,X^2+X+1)

let o be object ; :: thesis: ( o in {zeta,(zeta ^2)} implies b₁ in Roots (F_Complex,X^2+X+1) )
assume B: o in {zeta,(zeta ^2)} ; :: thesis: b₁ in Roots (F_Complex,X^2+X+1)
then reconsider c = o as Element of F_Complex ;

per cases ( o = zeta or o = zeta ^2 ) by B, TARSKI:def 2;

suppose E0: o = zeta ; :: thesis: b₁ in Roots (F_Complex,X^2+X+1)

E1: Re (zeta + 1) = (- (1 / 2)) + (Re 1r) by D1, COMPLEX1:8, COMPLEX1:def 4
.= 1 / 2 by COMPLEX1:6 ;
E2: Im (zeta + 1) = ((sqrt 3) / 2) + (Im 1r) by D1, COMPLEX1:8, COMPLEX1:def 4
.= (sqrt 3) / 2 by COMPLEX1:6 ;
E3: Re ((zeta |^ 2) + (zeta + 1)) = (- (1 / 2)) + (1 / 2) by K, D2, E1, COMPLEX1:8
.= 0 ;
E4: Im ((zeta |^ 2) + (zeta + 1)) = (- ((sqrt 3) / 2)) + ((sqrt 3) / 2) by K, D3, E2, COMPLEX1:8
.= 0 ;
E5: ((zeta |^ 2) + zeta) + 1 = 0c by E3, E4, COMPLEX1:4, COMPLEX1:3;
Ext_eval (X^2+X+1,c) = ((zeta |^ 2) + zeta) + 1 by E0, evalext11
.= 0. F_Complex by E5, COMPLFLD:def 1 ;
then c is_a_root_of X^2+X+1 , F_Complex by FIELD_4:def 2;
hence o in Roots (F_Complex,X^2+X+1) by H; :: thesis: verum

end;

suppose E0: o = zeta ^2 ; :: thesis: b₁ in Roots (F_Complex,X^2+X+1)

F: (zeta ^2) |^ 2 = (zeta ^2) * (zeta * zeta) by K1, O_RING_1:def 1
.= (zeta * zeta) * (zeta * zeta) by O_RING_1:def 1 ;
E1: Re ((zeta * zeta) + 1) = (- (1 / 2)) + (Re 1r) by D2, COMPLEX1:8, COMPLEX1:def 4
.= 1 / 2 by COMPLEX1:6 ;
E2: Im ((zeta * zeta) + 1) = (- ((sqrt 3) / 2)) + (Im 1r) by D3, COMPLEX1:8, COMPLEX1:def 4
.= - ((sqrt 3) / 2) by COMPLEX1:6 ;
E3: Re ((zeta * zeta) * (zeta * zeta)) = ((- (1 / 2)) * (- (1 / 2))) - ((- ((sqrt 3) / 2)) * (- ((sqrt 3) / 2))) by D2, D3, COMPLEX1:9
.= (1 / 4) - (((sqrt 3) * (sqrt 3)) / (2 * 2))
.= (1 / 4) - (((sqrt 3) ^2) / (2 * 2)) by SQUARE_1:def 1
.= (1 / 4) - (3 / 4) by SQUARE_1:def 2
.= - (1 / 2) ;
E4: Im ((zeta * zeta) * (zeta * zeta)) = ((- (1 / 2)) * (- ((sqrt 3) / 2))) + ((- (1 / 2)) * (- ((sqrt 3) / 2))) by D2, D3, COMPLEX1:9
.= (sqrt 3) / 2 ;
E5: Re (((zeta * zeta) * (zeta * zeta)) + ((zeta * zeta) + 1)) = (1 / 2) + (- (1 / 2)) by E1, E3, COMPLEX1:8
.= 0 ;
E6: Im (((zeta * zeta) * (zeta * zeta)) + ((zeta * zeta) + 1)) = ((sqrt 3) / 2) + (- ((sqrt 3) / 2)) by E2, E4, COMPLEX1:8
.= 0 ;
E7: (((zeta * zeta) * (zeta * zeta)) + (zeta * zeta)) + 1 = 0c by E5, E6, COMPLEX1:4, COMPLEX1:3;
Ext_eval (X^2+X+1,c) = (((zeta ^2) |^ 2) + (zeta ^2)) + 1 by E0, evalext11
.= (((zeta ^2) |^ 2) + (zeta * zeta)) + 1 by O_RING_1:def 1
.= 0. F_Complex by F, E7, COMPLFLD:def 1 ;
then c is_a_root_of X^2+X+1 , F_Complex by FIELD_4:def 2;
hence o in Roots (F_Complex,X^2+X+1) by H; :: thesis: verum

end;

end;

end;

then B: {zeta,(zeta ^2)} c= Roots (F_Complex,X^2+X+1) ;
the carrier of (Polynom-Ring F_Rat) c= the carrier of (Polynom-Ring F_Complex) by FIELD_4:10;
then reconsider q = X^2+X+1 as Element of the carrier of (Polynom-Ring F_Complex) ;
reconsider qq = q as non zero Element of the carrier of (Polynom-Ring F_Rat) ;
1. F_Rat <> 0. F_Rat ;
then H: 2 = deg X^2+X+1 by FIELD_9:18
.= deg q by FIELD_4:20 ;
then reconsider q = q as non constant Element of the carrier of (Polynom-Ring F_Complex) by RING_4:def 4;
C: card {zeta,(zeta ^2)} = 2

proof

now :: thesis: not zeta = zeta ^2

assume D6: zeta = zeta ^2 ; :: thesis: contradiction
zeta |^ (2 + 1) = (zeta |^ 2) * (zeta |^ 1) by BINOM:10
.= (zeta |^ 2) * zeta by BINOM:8
.= zeta |^ 2 by D6, K, O_RING_1:def 1 ;
hence contradiction by LZ23; :: thesis: verum

end;

hence card {zeta,(zeta ^2)} = 2 by CARD_2:57; :: thesis: verum

end;

D: card (Roots (F_Complex,X^2+X+1)) = 2

proof

F: card (Roots q) <= 2 by H, RING_5:22;
G: 2 <= card (Roots (F_Complex,qq)) by C, B, NAT_1:43;
Roots (F_Complex,X^2+X+1) = Roots q by FIELD_7:13;
hence card (Roots (F_Complex,X^2+X+1)) = 2 by F, G, XXREAL_0:1; :: thesis: verum

end;

thus Roots (F_Complex,X^2+X+1) = {zeta,(zeta ^2)} by B, C, D, lemfinset; :: thesis: verum