B: (sqrt 3) / 2 <> 0 by SQUARE_1:24;
((- 1) + (<i> * (sqrt 3))) / 2 = ((- 1) / 2) + (<i> * ((sqrt 3) / 2)) ;
then Im zeta <> 0 by B, COMPLEX1:12;
then not zeta in the carrier of F_Real ;
hence not zeta is F_Real -membered by FIELD_7:def 5; :: thesis: zeta is F_Rat -algebraic
thus zeta is F_Rat -algebraic by LL33, FIELD_6:43; :: thesis: verum