Ext_eval (X^2-2,2-Root(2)) = (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_Real ;
hence MinPoly (2-Root(2),F_Rat) = X^2-2 by FIELD_6:52; :: thesis: verum