theorem evalext2: :: FIELD_10:26

for z being Element of F_Complex holds Ext_eval (X^3-2,z) = (z |^ 3) - 2