let z be Element of the carrier of F_Complex; :: thesis: ( Ext_eval (X^3-1,z) = 0. F_Complex iff z is CRoot of 3,1 )
reconsider z1 = z as Complex ;

A: now :: thesis: ( Ext_eval (X^3-1,z) = 0. F_Complex implies z is CRoot of 3,1 )

assume Ext_eval (X^3-1,z) = 0. F_Complex ; :: thesis: z is CRoot of 3,1
then (z |^ 3) - 1 = 0. F_Complex by evalext1
.= 0 by COMPLFLD:def 1 ;
then 1 = z1 |^ 3 by lem3c;
hence z is CRoot of 3,1 by COMPTRIG:def 2; :: thesis: verum

end;

now :: thesis: ( z is CRoot of 3,1 implies Ext_eval (X^3-1,z) = 0. F_Complex )

assume z is CRoot of 3,1 ; :: thesis: Ext_eval (X^3-1,z) = 0. F_Complex
then 1 = z1 |^ 3 by COMPTRIG:def 2
.= z |^ 3 by lem3c ;
hence Ext_eval (X^3-1,z) = 1 - 1 by evalext1
.= 0. F_Complex by COMPLFLD:def 1 ;
:: thesis: verum

end;

hence ( Ext_eval (X^3-1,z) = 0. F_Complex iff z is CRoot of 3,1 ) by A; :: thesis: verum