:: deftheorem defines X^2-2 FIELD_10:def 1 :
X^2-2 = <%(- ((1. F_Rat) + (1. F_Rat))),(0. F_Rat),(1. F_Rat)%>;