theorem :: FIELD_10:20

for x being Element of F_Rat holds eval (X^3-1,x) = (x |^ 3) - 1 by LL31;