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