theorem :: FIELD_10:25

for z being Element of F_Complex holds Ext_eval (X^2+X+1,z) = ((z |^ 2) + z) + 1 by evalext11;