set F = FAdj (F_Rat,{zeta});
Roots (F_Complex,X^3-1) c= the carrier of (FAdj (F_Rat,{zeta}))

proof

A1: {zeta} is Subset of (FAdj (F_Rat,{zeta})) by FIELD_6:35;
zeta in {zeta} by TARSKI:def 1;
then reconsider b = zeta as Element of (FAdj (F_Rat,{zeta})) by A1;
A3: FAdj (F_Rat,{zeta}) is Subring of F_Complex by FIELD_5:12;
A4: zeta ^2 = zeta * zeta by O_RING_1:def 1
.= b * b by A3, FIELD_6:16 ;

now :: thesis: for o being object st o in Roots (F_Complex,X^3-1) holds
o in the carrier of (FAdj (F_Rat,{zeta}))

let o be object ; :: thesis: ( o in Roots (F_Complex,X^3-1) implies b₁ in the carrier of (FAdj (F_Rat,{zeta})) )
assume o in Roots (F_Complex,X^3-1) ; :: thesis: b₁ in the carrier of (FAdj (F_Rat,{zeta}))

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

suppose o = 1 ; :: thesis: b₁ in the carrier of (FAdj (F_Rat,{zeta}))

then o = 1. F_Complex by COMPLEX1:def 4, COMPLFLD:def 1
.= 1. (FAdj (F_Rat,{zeta})) by EC_PF_1:def 1 ;
hence o in the carrier of (FAdj (F_Rat,{zeta})) ; :: thesis: verum

end;

suppose o = zeta ; :: thesis: b₁ in the carrier of (FAdj (F_Rat,{zeta}))

then o = b ;
hence o in the carrier of (FAdj (F_Rat,{zeta})) ; :: thesis: verum

end;

suppose o = zeta ^2 ; :: thesis: b₁ in the carrier of (FAdj (F_Rat,{zeta}))

hence o in the carrier of (FAdj (F_Rat,{zeta})) by A4; :: thesis: verum

end;

end;

end;

hence Roots (F_Complex,X^3-1) c= the carrier of (FAdj (F_Rat,{zeta})) ; :: thesis: verum

end;

then B: X^3-1 splits_in FAdj (F_Rat,{zeta}) by LLsplit, FIELD_8:27;

now :: thesis: for E being FieldExtension of F_Rat st X^3-1 splits_in E & E is Subfield of FAdj (F_Rat,{zeta}) holds
E == FAdj (F_Rat,{zeta})

let E be FieldExtension of F_Rat ; :: thesis: ( X^3-1 splits_in E & E is Subfield of FAdj (F_Rat,{zeta}) implies E == FAdj (F_Rat,{zeta}) )
assume C: ( X^3-1 splits_in E & E is Subfield of FAdj (F_Rat,{zeta}) ) ; :: thesis: E == FAdj (F_Rat,{zeta})
then E: E is Subfield of F_Complex by EC_PF_1:5;
D: F_Rat is Subfield of E by FIELD_4:7;
{zeta} is Subset of E

proof

F_Complex is E -extending by E, FIELD_4:7;
then A1: Roots (F_Complex,X^3-1) c= the carrier of E by LLsplit, C, FIELD_8:27;
zeta in Roots (F_Complex,X^3-1) by lemroots3, ENUMSET1:def 1;
then zeta in the carrier of E by A1;
then {zeta} c= the carrier of E by TARSKI:def 1;
hence {zeta} is Subset of E ; :: thesis: verum

end;

then FAdj (F_Rat,{zeta}) is Subfield of E by D, E, FIELD_6:37;
hence E == FAdj (F_Rat,{zeta}) by C, FIELD_7:def 2; :: thesis: verum

end;

hence FAdj (F_Rat,{zeta}) is SplittingField of X^3-1 by B, FIELD_8:def 1; :: thesis: verum