let z be complex number ; :: thesis: for n0 being non zero natural number holds (n0 -root z) |^ n0 = z
let n0 be non zero natural number ; :: thesis: (n0 -root z) |^ n0 = z
reconsider n = n0 as Element of NAT by ORDINAL1:def 13;
thus (n0 -root z) |^ n0 = (((n -real-root |.z.|) * (cos (((Arg z) + ((2 * PI ) * 0 )) / n))) + (((n -real-root |.z.|) * (sin (((Arg z) + ((2 * PI ) * 0 )) / n))) * <i> )) |^ n
.= z by POLYEQ_3:56 ; :: thesis: verum