set F = F_Complex ;
set p = X^3-1 ;
set M = {1,zeta,(zeta ^2)};
reconsider z = zeta as Complex ;
H: Roots (F_Complex,X^3-1) = { a where a is Element of F_Complex : a is_a_root_of X^3-1 , F_Complex } by FIELD_4:def 4;
Z: 1 = 1. F_Complex by COMPLFLD:def 1, COMPLEX1:def 4;

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

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

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

suppose E0: o = 1 ; :: thesis: b₁ in Roots (F_Complex,X^3-1)

Ext_eval (X^3-1,(1. F_Complex)) = ((1. F_Complex) |^ 3) - 1 by evalext1
.= ((1. F_Complex) |^ (2 + 1)) - (1. F_Complex) by Z, COMPLFLD:2
.= (((1. F_Complex) |^ 2) * ((1. F_Complex) |^ 1)) - (1. F_Complex) by BINOM:10
.= (((1. F_Complex) |^ (1 + 1)) * (1. F_Complex)) - (1. F_Complex) by BINOM:8
.= (((1. F_Complex) |^ 1) * ((1. F_Complex) |^ 1)) - (1. F_Complex) by BINOM:10
.= (((1. F_Complex) |^ 1) * (1. F_Complex)) - (1. F_Complex) by BINOM:8
.= (1. F_Complex) - (1. F_Complex) by BINOM:8
.= 0. F_Complex by RLVECT_1:5 ;
then 1. F_Complex is_a_root_of X^3-1 , F_Complex by FIELD_4:def 2;
hence o in Roots (F_Complex,X^3-1) by H, E0, Z; :: thesis: verum

end;

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

Ext_eval (X^3-1,zeta) = 0. F_Complex by lemCRo, lemCRo2;
then zeta is_a_root_of X^3-1 , F_Complex by FIELD_4:def 2;
hence o in Roots (F_Complex,X^3-1) by H, E0; :: thesis: verum

end;

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

Ext_eval (X^3-1,(zeta ^2)) = 0. F_Complex by lemCRo, lemCRo2;
then zeta ^2 is_a_root_of X^3-1 , F_Complex by FIELD_4:def 2;
hence o in Roots (F_Complex,X^3-1) by H, E0; :: thesis: verum

end;

end;

end;

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

proof

D0: zeta = (- (1 / 2)) + (<i> * ((sqrt 3) / 2)) ;
then ( Re zeta = - (1 / 2) & Im zeta = (sqrt 3) / 2 ) by COMPLEX1:12;
then D2: Im (zeta * zeta) = 2 * ((- (1 / 2)) * ((sqrt 3) / 2)) by COMPLEX1:16
.= - ((sqrt 3) / 2) ;
D3: (sqrt 3) / 2 <> 0 by SQUARE_1:24;
C1: zeta <> 1 by D0, COMPLEX1:12, COMPLEX1:6, COMPLEX1:def 4;

C2: now :: thesis: not 1 = zeta ^2

assume 1 = zeta ^2 ; :: thesis: contradiction
then zeta * zeta = 1. F_Complex by Z, O_RING_1:def 1
.= 1r by COMPLFLD:def 1 ;
hence contradiction by D2, D3, COMPLEX1:6; :: thesis: verum

end;

C3: now :: thesis: not zeta = zeta ^2

assume zeta = zeta ^2 ; :: thesis: contradiction
then zeta * (1. F_Complex) = zeta * zeta by O_RING_1:def 1;
then zeta = 1. F_Complex by E1, VECTSP_2:8
.= 1r by COMPLFLD:def 1 ;
hence contradiction by D0, COMPLEX1:12, COMPLEX1:6; :: thesis: verum

end;

thus card {1,zeta,(zeta ^2)} = 3 by C1, C2, C3, CARD_2:58; :: thesis: verum

end;

D: card (Roots (F_Complex,X^3-1)) = 3

proof

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

end;

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