let e be CRoot of n,x; :: thesis: e is Element of F_Complex
e is Element of COMPLEX by XCMPLX_0:def 2;
hence e is Element of F_Complex by Def1; :: thesis: verum