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