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