theorem :: FIELD_10:23

for r being Element of F_Real holds Ext_eval (X^2-2,r) = (r |^ 2) - 2 by LKX2ext;