theorem :: FIELD_10:27

for z being Element of the carrier of F_Complex holds
( Ext_eval (X^3-1,z) = 0. F_Complex iff z is CRoot of 3,1 ) by lemCRo;