let z be Complex; :: thesis: for n, k being 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 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 A3: 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

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.|) + (0 * <i>)) * ((cos (((Arg z) + ((2 * PI) * k)) / n)) + ((sin (((Arg z) + ((2 * PI) * k)) / n)) * <i>))) |^ n
.= (((n -root |.z.|) + (0 * <i>)) |^ n) * (((cos (((Arg z) + ((2 * PI) * k)) / n)) + ((sin (((Arg z) + ((2 * PI) * k)) / n)) * <i>)) |^ n) by NEWTON:7
.= (((n -root |.z.|) + (0 * <i>)) |^ n) * ((cos (Arg z)) + ((sin (Arg z)) * <i>)) by A1, Th55
.= (|.z.| + (0 * <i>)) * ((cos (Arg z)) + ((sin (Arg z)) * <i>)) by A1, Th4, COMPLEX1:46
.= ((|.z.| * (cos (Arg z))) - (0 * (sin (Arg z)))) + (((|.z.| * (sin (Arg z))) + (0 * (cos (Arg z)))) * <i>)
.= z by A3, Def1 ; :: 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 + ((0 * (sin (((Arg z) + ((2 * PI) * k)) / n))) * <i>)) |^ n by A2, POWER:5
.= z by A2, A4, NEWTON:11 ;
:: thesis: verum

end;

end;