let z be Complex; :: thesis: for n, k being Element of NAT st n <> 0 holds
z = (((n -root |.z.|) * (cos (((Arg z) + ((2 * PI) * k)) / n))) + (((n -root |.z.|) * (sin (((Arg z) + ((2 * PI) * k)) / n))) * <i>)) |^ n
let n, k be Element of NAT ; :: thesis: ( n <> 0 implies z = (((n -root |.z.|) * (cos (((Arg z) + ((2 * PI) * k)) / n))) + (((n -root |.z.|) * (sin (((Arg z) + ((2 * PI) * k)) / n))) * <i>)) |^ n )
assume A1: n <> 0 ; :: thesis: z = (((n -root |.z.|) * (cos (((Arg z) + ((2 * PI) * k)) / n))) + (((n -root |.z.|) * (sin (((Arg z) + ((2 * PI) * k)) / n))) * <i>)) |^ n
then A2: n >= 0 + 1 by NAT_1:13;

per cases ( z <> 0 or z = 0 ) ;

suppose z <> 0 ; :: thesis: z = (((n -root |.z.|) * (cos (((Arg z) + ((2 * PI) * k)) / n))) + (((n -root |.z.|) * (sin (((Arg z) + ((2 * PI) * k)) / n))) * <i>)) |^ n

then A3: |.z.| > 0 by COMPLEX1:47;
thus (((n -root |.z.|) * (cos (((Arg z) + ((2 * PI) * k)) / n))) + (((n -root |.z.|) * (sin (((Arg z) + ((2 * PI) * k)) / n))) * <i>)) |^ n = ((n -root |.z.|) * ((cos (((Arg z) + ((2 * PI) * k)) / n)) + ((sin (((Arg z) + ((2 * PI) * k)) / n)) * <i>))) |^ n
.= ((n -root |.z.|) |^ n) * (((cos (((Arg z) + ((2 * PI) * k)) / n)) + ((sin (((Arg z) + ((2 * PI) * k)) / n)) * <i>)) |^ n) by NEWTON:7
.= ((n -root |.z.|) |^ n) * ((cos (Arg z)) + ((sin (Arg z)) * <i>)) by A1, Th33
.= |.z.| * ((cos (Arg z)) + ((sin (Arg z)) * <i>)) by A1, A3, COMPTRIG:4
.= ((|.z.| * (cos (Arg z))) - (0 * (sin (Arg z)))) + (((|.z.| * (sin (Arg z))) + (0 * (cos (Arg z)))) * <i>)
.= z by COMPTRIG:62 ; :: thesis: verum

end;

suppose A4: z = 0 ; :: thesis: z = (((n -root |.z.|) * (cos (((Arg z) + ((2 * PI) * k)) / n))) + (((n -root |.z.|) * (sin (((Arg z) + ((2 * PI) * k)) / n))) * <i>)) |^ n

hence (((n -root |.z.|) * (cos (((Arg z) + ((2 * PI) * k)) / n))) + (((n -root |.z.|) * (sin (((Arg z) + ((2 * PI) * k)) / n))) * <i>)) |^ n = ((0 * (cos (((Arg z) + ((2 * PI) * k)) / n))) + (((n -root 0) * (sin (((Arg z) + ((2 * PI) * k)) / n))) * <i>)) |^ n by A2, COMPLEX1:44, POWER:5
.= ((0 * (sin (((Arg z) + ((2 * PI) * k)) / n))) * <i>) |^ n by A2, POWER:5
.= z by A1, A4, Lm2 ;
:: thesis: verum

end;

end;