set F = FAdj ((Z/ 2),{alpha});
H: embField (canHomP X^2+X+1) is FieldExtension of FAdj ((Z/ 2),{alpha}) by FIELD_4:7;
( alpha in {alpha} & {alpha} is Subset of (FAdj ((Z/ 2),{alpha})) ) by TARSKI:def 1, FIELD_6:35;
then reconsider a = alpha as Element of (FAdj ((Z/ 2),{alpha})) ;
alpha " = a " by FIELD_6:18;
then reconsider ai = alpha " as Element of (FAdj ((Z/ 2),{alpha})) ;
C: ( rpoly (1,alpha) = rpoly (1,a) & rpoly (1,(alpha ")) = rpoly (1,ai) ) by H, FIELD_4:21;
reconsider q = (rpoly (1,a)) *' (rpoly (1,ai)) as Element of the carrier of (Polynom-Ring (FAdj ((Z/ 2),{alpha}))) by POLYNOM3:def 10;
A: X^2+X+1 = (rpoly (1,a)) *' (rpoly (1,ai)) by H, C, lemZ2, FIELD_4:17;
( Roots (rpoly (1,a)) = {a} & Roots (rpoly (1,ai)) = {ai} ) by RING_5:18;
then Roots ((rpoly (1,a)) *' (rpoly (1,ai))) = {a} \/ {ai} by UPROOTS:23
.= {a,ai} by ENUMSET1:1 ;
then {a,ai} = Roots q
.= Roots ((FAdj ((Z/ 2),{alpha})),X^2+X+1) by A, FIELD_7:13 ;
hence Roots ((FAdj ((Z/ 2),{alpha})),X^2+X+1) = {alpha,alpha-1} by lemalph; :: thesis: verum