theorem :: FIELD_10:22

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