let n be non zero Element of NAT ; :: thesis: ex x being Element of (MultGroup F_Complex) st ord x = n
set x = [**(cos (((2 * PI) * 1) / n)),(sin (((2 * PI) * 1) / n))**];
( n -roots_of_1 c= the carrier of (MultGroup F_Complex) & [**(cos (((2 * PI) * 1) / n)),(sin (((2 * PI) * 1) / n))**] in n -roots_of_1 ) by Th24, Th32;
then reconsider y = [**(cos (((2 * PI) * 1) / n)),(sin (((2 * PI) * 1) / n))**] as Element of (MultGroup F_Complex) ;
( ord y = n div (1 gcd n) & 1 gcd n = 1 ) by Th31, WSIERP_1:8;
hence ex x being Element of (MultGroup F_Complex) st ord x = n by NAT_2:4; :: thesis: verum