set t = - ((1. F_Rat) + (1. F_Rat));
let x be Element of F_Rat; :: thesis: eval (X^2-2,x) = (x |^ 2) - 2
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))),(0. F_Rat),(1. F_Rat)%>,x) = ((- ((1. F_Rat) + (1. F_Rat))) + ((0. F_Rat) * x)) + ((1. F_Rat) * (x ^2)) by FIELD_9:20;
hence eval (X^2-2,x) = (x |^ 2) - 2 by H, GAUSSINT:def 14; :: thesis: verum