let x be Element of COMPLEX ; :: thesis: for n being non zero Nat
for k being Nat holds ((n -root |.x.|) * (cos (((Arg x) + ((2 * PI) * k)) / n))) + (((n -root |.x.|) * (sin (((Arg x) + ((2 * PI) * k)) / n))) * <i>) is CRoot of n,x
let n be non zero Nat; :: thesis: for k being Nat holds ((n -root |.x.|) * (cos (((Arg x) + ((2 * PI) * k)) / n))) + (((n -root |.x.|) * (sin (((Arg x) + ((2 * PI) * k)) / n))) * <i>) is CRoot of n,x
let k be Nat; :: thesis: ((n -root |.x.|) * (cos (((Arg x) + ((2 * PI) * k)) / n))) + (((n -root |.x.|) * (sin (((Arg x) + ((2 * PI) * k)) / n))) * <i>) is CRoot of n,x
reconsider z = ((n -root |.x.|) * (cos (((Arg x) + ((2 * PI) * k)) / n))) + (((n -root |.x.|) * (sin (((Arg x) + ((2 * PI) * k)) / n))) * <i>) as Element of COMPLEX by XCMPLX_0:def 2;
z |^ n = x by Th56;
hence ((n -root |.x.|) * (cos (((Arg x) + ((2 * PI) * k)) / n))) + (((n -root |.x.|) * (sin (((Arg x) + ((2 * PI) * k)) / n))) * <i>) is CRoot of n,x by Def2; :: thesis: verum