not sqrt 2 in RAT by INT_2:28, IRRAT_1:1;
hence not 2-CRoot(2) is F_Rat -membered by FIELD_7:def 5, GAUSSINT:def 14; :: thesis: 2-CRoot(2) is F_Rat -algebraic
Ext_eval (X^2-2,2-CRoot(2)) = Ext_eval (X^2-2,2-Root(2)) by FIELD_7:14
.= (2-Root(2) |^ (1 + 1)) - 2 by LKX2ext
.= ((2-Root(2) |^ 1) * (2-Root(2) |^ 1)) - 2 by BINOM:10
.= (2-Root(2) * (2-Root(2) |^ 1)) - 2 by BINOM:8
.= (2-Root(2) * 2-Root(2)) - 2 by BINOM:8
.= ((sqrt 2) ^2) - 2 by SQUARE_1:def 1
.= 2 - 2 by SQUARE_1:def 2
.= 0. F_Complex by COMPLFLD:def 1 ;
hence 2-CRoot(2) is F_Rat -algebraic by FIELD_6:43; :: thesis: verum