let x be Element of F_Rat; :: thesis: eval (X^2+X+1,x) = ((x |^ 2) + x) + 1
H: x ^2 = x * x by O_RING_1:def 1
.= (x |^ 1) * x by BINOM:8
.= (x |^ 1) * (x |^ 1) by BINOM:8
.= x |^ (1 + 1) by BINOM:10 ;
eval (<%(1. F_Rat),(1. F_Rat),(1. F_Rat)%>,x) = ((1. F_Rat) + ((1. F_Rat) * x)) + ((1. F_Rat) * (x ^2)) by FIELD_9:20;
hence eval (X^2+X+1,x) = ((x |^ 2) + x) + 1 by H, GAUSSINT:def 14; :: thesis: verum