set F = embField (canHomP X^2+X+1);
A0: Z/ 2 is Subring of embField (canHomP X^2+X+1) by FIELD_4:def 1;
the carrier of (Polynom-Ring (Z/ 2)) c= the carrier of (Polynom-Ring (embField (canHomP X^2+X+1))) by FIELD_4:10;
then reconsider p = X^2+X+1 as Element of the carrier of (Polynom-Ring (embField (canHomP X^2+X+1))) ;
eval (p,alpha) = Ext_eval (X^2+X+1,alpha) by FIELD_4:26
.= 0. (Z/ 2) by FIELD_5:17
.= 0. (embField (canHomP X^2+X+1)) by A0, C0SP1:def 3 ;
then alpha is_a_root_of p ;
then consider q being Polynomial of (embField (canHomP X^2+X+1)) such that
A1: p = (rpoly (1,alpha)) *' q by HURWITZ:33;

H0: now :: thesis: not q = 0_. (embField (canHomP X^2+X+1))

assume H1: q = 0_. (embField (canHomP X^2+X+1)) ; :: thesis: contradiction
deg p = deg X^2+X+1 by FIELD_4:20;
hence contradiction by H1, A1, HURWITZ:20; :: thesis: verum

end;

H1: alpha <> 0. (embField (canHomP X^2+X+1)) ;
2 = deg X^2+X+1 by qua4
.= deg p by FIELD_4:20
.= (deg (rpoly (1,alpha))) + (deg q) by A1, H0, HURWITZ:23
.= 1 + (deg q) by HURWITZ:27 ;
then consider x, b being Element of (embField (canHomP X^2+X+1)) such that
A2: ( x <> 0. (embField (canHomP X^2+X+1)) & q = x * (rpoly (1,b)) ) by HURWITZ:28;
A3: ( rpoly (1,b) = <%(- b),(1. (embField (canHomP X^2+X+1)))%> & rpoly (1,alpha) = <%(- alpha),(1. (embField (canHomP X^2+X+1)))%> ) by RING_5:10;
then q = <%(x * (- b)),(x * (1. (embField (canHomP X^2+X+1))))%> by A2, qua20;
then A4: p = <%((- alpha) * (x * (- b))),(((1. (embField (canHomP X^2+X+1))) * (x * (- b))) + ((x * (1. (embField (canHomP X^2+X+1)))) * (- alpha))),((1. (embField (canHomP X^2+X+1))) * (x * (1. (embField (canHomP X^2+X+1)))))%> by A1, A3, lemred1
.= <%((- alpha) * (x * (- b))),((x * (- b)) + (x * (- alpha))),x%> ;
then A5: x = X^2+X+1 . 2 by qua1
.= 1. (Z/ 2) by qua1
.= 1. (embField (canHomP X^2+X+1)) by A0, C0SP1:def 3 ;
then p = <%(alpha * b),((- b) + (- alpha)),(1. (embField (canHomP X^2+X+1)))%> by A4, VECTSP_1:10;
then alpha * b = X^2+X+1 . 0 by qua1
.= 1. (Z/ 2) by qua1
.= 1. (embField (canHomP X^2+X+1)) by A0, C0SP1:def 3 ;
then A7: b * alpha = 1. (embField (canHomP X^2+X+1)) by GROUP_1:def 12;
then A6: b = alpha " by H1, VECTSP_1:def 10;
thus X^2+X+1 = (X- alpha) *' (X- (alpha ")) by A1, A5, A7, A2, VECTSP_1:def 10; :: thesis: ( alpha " = - (alpha + (1. (embField (canHomP X^2+X+1)))) & - alpha = (alpha ") + (1. (embField (canHomP X^2+X+1))) )
- (b + alpha) = (- b) + (- alpha) by RLVECT_1:31
.= p . 1 by A4, A5, qua1
.= 1. (Z/ 2) by qua1
.= 1. (embField (canHomP X^2+X+1)) by A0, C0SP1:def 3 ;
then b + (alpha + (- alpha)) = (- alpha) - (1. (embField (canHomP X^2+X+1))) by RLVECT_1:def 3;
then A8: (alpha ") + (0. (embField (canHomP X^2+X+1))) = (- alpha) + (- (1. (embField (canHomP X^2+X+1)))) by A6, RLVECT_1:5;
hence alpha " = (- alpha) - (1. (embField (canHomP X^2+X+1)))
.= - (alpha + (1. (embField (canHomP X^2+X+1)))) by RLVECT_1:30 ;
:: thesis: - alpha = (alpha ") + (1. (embField (canHomP X^2+X+1)))
(alpha ") + (1. (embField (canHomP X^2+X+1))) = (- alpha) + ((- (1. (embField (canHomP X^2+X+1)))) + (1. (embField (canHomP X^2+X+1)))) by A8, RLVECT_1:def 3
.= (- alpha) + (0. (embField (canHomP X^2+X+1))) by RLVECT_1:5 ;
hence - alpha = (alpha ") + (1. (embField (canHomP X^2+X+1))) ; :: thesis: verum