theorem :: FIELD_10:21

for x being Element of F_Rat holds eval (X^2+X+1,x) = ((x |^ 2) + x) + 1 by LL32;