theorem :: FIELD_10:24

for z being Element of F_Complex holds Ext_eval (X^3-1,z) = (z |^ 3) - 1 by evalext1;