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