the carrier of F_Complex = COMPLEX by COMPLFLD:def 1;
then reconsider z = ((- 1) + (<i> * (sqrt 3))) / 2 as Element of F_Complex by XCMPLX_0:def 2;
H: (sqrt 3) / 2 <> 0 by SQUARE_1:24;
z = (- (1 / 2)) + (<i> * ((sqrt 3) / 2)) ;
then Im z = (sqrt 3) / 2 by COMPLEX1:12;
then z <> 0c by H;
then not z is zero by COMPLFLD:def 1;
hence ((- 1) + (<i> * (sqrt 3))) / 2 is non zero Element of F_Complex ; :: thesis: verum