:: deftheorem defines X^3-2 FIELD_10:def 3 :
X^3-2 = ((0_. F_Rat) +* (0,(- 2))) +* (3,1);