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