reconsider z = ((n -root |.x.|) * (cos (((Arg x) + ((2 * PI) * 0)) / n))) + (((n -root |.x.|) * (sin (((Arg x) + ((2 * PI) * 0)) / n))) * <i>) as Element of COMPLEX by XCMPLX_0:def 2;
take z ; :: thesis: z |^ n = x
thus z |^ n = x by Th56; :: thesis: verum