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