A: now :: thesis: for o being object st o in {1} holds
o in Roots X^3-1

let o be object ; :: thesis: ( o in {1} implies o in Roots X^3-1 )
assume o in {1} ; :: thesis: o in Roots X^3-1
then B: o = 1. F_Rat by TARSKI:def 1, GAUSSINT:13;
eval (X^3-1,(1. F_Rat)) = ((1. F_Rat) |^ (2 + 1)) - (1. F_Rat) by LL31, GAUSSINT:13
.= (((1. F_Rat) |^ 2) * ((1. F_Rat) |^ 1)) - (1. F_Rat) by BINOM:10
.= (((1. F_Rat) |^ (1 + 1)) * (1. F_Rat)) - (1. F_Rat) by BINOM:8
.= (((1. F_Rat) |^ 1) * ((1. F_Rat) |^ 1)) - (1. F_Rat) by BINOM:10
.= (((1. F_Rat) |^ 1) * (1. F_Rat)) - (1. F_Rat) by BINOM:8
.= ((1. F_Rat) * (1. F_Rat)) - (1. F_Rat) by BINOM:8
.= 0. F_Rat by RLVECT_1:15 ;
then 1. F_Rat is_a_root_of X^3-1 by POLYNOM5:def 7;
hence o in Roots X^3-1 by B, POLYNOM5:def 10; :: thesis: verum

end;

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;

now :: thesis: for o being object st o in Roots X^3-1 holds
o in {1}

let o be object ; :: thesis: ( o in Roots X^3-1 implies o in {1} )
assume C: o in Roots X^3-1 ; :: thesis: o in {1}
then reconsider a = o as Element of F_Rat ;
F_Rat is Subfield of F_Complex by FIELD_4:7;
then the carrier of F_Rat c= the carrier of F_Complex by EC_PF_1:def 1;
then reconsider c = a as Element of F_Complex ;
G: a is_a_root_of X^3-1 by C, POLYNOM5:def 10;
0. F_Complex = 0. F_Rat by GAUSSINT:13, COMPLFLD:def 1
.= eval (X^3-1,a) by G, POLYNOM5:def 7
.= Ext_eval (X^3-1,c) by FIELD_6:10 ;
then c is_a_root_of X^3-1 , F_Complex by FIELD_4:def 2;
then D: a in {1,zeta,(zeta ^2)} by H, lemroots3;
F_Rat is Subfield of F_Real by FIELD_4:7;
then E: the carrier of F_Rat c= the carrier of F_Real by EC_PF_1:def 1;

now :: thesis: not a <> 1

assume a <> 1 ; :: thesis: contradiction

per cases then ( a = zeta or a = zeta ^2 ) by D, ENUMSET1:def 1;

suppose a = zeta ; :: thesis: contradiction

hence contradiction by E, FIELD_7:def 5; :: thesis: verum

end;

suppose a = zeta ^2 ; :: thesis: contradiction

hence contradiction by E, FIELD_7:def 5; :: thesis: verum

end;

end;

end;

hence o in {1} by TARSKI:def 1; :: thesis: verum

end;

hence Roots X^3-1 = {1} by A, TARSKI:2; :: thesis: verum