H: Roots (F_Complex,X^2+X+1) = { a where a is Element of F_Complex : a is_a_root_of X^2+X+1 , F_Complex } by FIELD_4:def 4;
zeta in Roots (F_Complex,X^2+X+1) by rootz, TARSKI:def 2;
then consider a being Element of F_Complex such that
I: ( a = zeta & a is_a_root_of X^2+X+1 , F_Complex ) by H;
Ext_eval (X^2+X+1,zeta) = 0. F_Complex by I, FIELD_4:def 2;
hence MinPoly (zeta,F_Rat) = X^2+X+1 by FIELD_6:52; :: thesis: verum