:: deftheorem defines X^2+X FIELD_9:def 14 :
X^2+X = <%(0. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%>;