:: deftheorem defines alpha-1 FIELD_9:def 19 :
alpha-1 = alpha - (1. (embField (canHomP X^2+X+1)));