z *' in COMPLEX by XCMPLX_0:def 2;
hence z *' is Element of F_Complex by Def1; :: thesis: verum