theorem :: FIELD_10:19

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