Char (Z/ 2) = 2
by RING_3:def 6;
then A:
2 '*' (1. (Z/ 2)) = 0. (Z/ 2)
by RING_3:def 5;
thus eval ((npoly ((Z/ 2),2)),(1. (Z/ 2))) =
((1. (Z/ 2)) |^ 2) + (1. (Z/ 2))
by lem1a
.=
((1. (Z/ 2)) * (1. (Z/ 2))) + (1. (Z/ 2))
by prl4
.=
0. (Z/ 2)
by A, prl3
; verum