let n be non zero Element of NAT ; :: thesis:
set X = { [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] where k is Element of NAT : k < n } ;

assume A1: x in n -roots_of_1 ; :: thesis:
then reconsider a = x as Element of F_Complex ;
consider k being Element of NAT such that
A2: a = [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] by A1, Th24;
A3: k mod n < n by NAT_D:1;
a = [**(cos (((2 * PI) * (k mod n)) / n)),(sin (((2 * PI) * (k mod n)) / n))**] by A2, Th10;
hence x in { [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] where k is Element of NAT : k < n } by A3; :: thesis:

end;

assume x in { [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] where k is Element of NAT : k < n } ; :: thesis:
then ex k being Element of NAT st
( x = [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] & k < n ) ;
hence x in n -roots_of_1 by Th24; :: thesis:

end;

hence n -roots_of_1 = { [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] where k is Element of NAT : k < n } by TARSKI:2; :: thesis: