H: Z/ 2 is Subring of embField (canHomP X^2+X+1) by FIELD_4:def 1;
Ext_eval (X^2+X+1,alpha) = 0. (Z/ 2) by FIELD_5:17
.= 0. (embField (canHomP X^2+X+1)) by H, C0SP1:def 3 ;
hence MinPoly (alpha,(Z/ 2)) = X^2+X+1 by FIELD_6:52; :: thesis: verum