let z be Complex; :: thesis: for n0 being non zero Nat holds (n0 -root z) |^ n0 = z
let n0 be non zero Nat; :: thesis: (n0 -root z) |^ n0 = z
reconsider n = n0 as Element of NAT by ORDINAL1:def 12;
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:34 ; :: thesis: verum