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

now :: thesis: for x being object holds
( ( x in n -roots_of_1 implies x in { [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] where k is Element of NAT : k < n } ) & ( x in { [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] where k is Element of NAT : k < n } implies x in n -roots_of_1 ) )

let x be object ; :: thesis: ( ( x in n -roots_of_1 implies x in { [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] where k is Element of NAT : k < n } ) & ( x in { [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] where k is Element of NAT : k < n } implies x in n -roots_of_1 ) )

hereby :: thesis: ( x in { [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] where k is Element of NAT : k < n } implies x in n -roots_of_1 )

assume A1: x in n -roots_of_1 ; :: thesis: x in { [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] where k is Element of NAT : k < n }
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: verum

end;

assume x in { [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] where k is Element of NAT : k < n } ; :: thesis: x in n -roots_of_1
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: verum

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: verum