H:
(sqrt 3) / 2 <> 0
by SQUARE_1:24;
I:
zeta * zeta = zeta ^2
by O_RING_1:def 1;
zeta = (- (1 / 2)) + (<i> * ((sqrt 3) / 2))
;
then
( Re zeta = - (1 / 2) & Im zeta = (sqrt 3) / 2 )
by COMPLEX1:12;
then Im (zeta * zeta) =
2 * ((- (1 / 2)) * ((sqrt 3) / 2))
by COMPLEX1:16
.=
- ((sqrt 3) / 2)
;
then
not zeta * zeta in the carrier of F_Real
by H;
hence
( not zeta ^2 is F_Real -membered & zeta ^2 is F_Rat -algebraic )
by I, FIELD_7:def 5; verum