A: X_ *' X-1 =
(rpoly (1,(- (0. (Z/ 2))))) *' <%(1. (Z/ 2)),(- (- (1. (Z/ 2))))%>
by RING_5:10
.=
(rpoly (1,(0. (Z/ 2)))) *' (rpoly (1,(1. (Z/ 2))))
by cz2a, RING_5:10
;
hence B: X_ *' X-1 =
<%((0. (Z/ 2)) * (1. (Z/ 2))),(- ((0. (Z/ 2)) + (1. (Z/ 2)))),(1. (Z/ 2))%>
by lemred3z
.=
X^2+X
by FIELD_3:4, RLVECT_1:def 10
;
Roots X^2+X = {(0. (Z/ 2)),(1. (Z/ 2))}
( Roots (rpoly (1,(1. (Z/ 2)))) = {(1. (Z/ 2))} & Roots (rpoly (1,(0. (Z/ 2)))) = {(0. (Z/ 2))} )
by RING_5:18;
then Roots ((rpoly (1,(0. (Z/ 2)))) *' (rpoly (1,(1. (Z/ 2))))) =
{(0. (Z/ 2))} \/ {(1. (Z/ 2))}
by UPROOTS:23
.=
{(0. (Z/ 2)),(1. (Z/ 2))}
by ENUMSET1:1
;
hence
Roots X^2+X = {(0. (Z/ 2)),(1. (Z/ 2))}
by A, B; verum