<i> * (sqrt 3) in COMPLEX by XCMPLX_0:def 2;
then reconsider t = <i> * (sqrt 3) as Element of F_Complex by COMPLFLD:def 1;
<i> * (sqrt 3) <> 0 by SQUARE_1:25;
then not t is zero by COMPLFLD:def 1;
hence <i> * (sqrt 3) is non zero Element of F_Complex ; :: thesis: verum