let n be non empty 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))**];
A1: n -roots_of_1 c= the carrier of (MultGroup F_Complex ) by Th35;
[**(cos (((2 * PI ) * 1) / n)),(sin (((2 * PI ) * 1) / n))**] in n -roots_of_1 by Th27;
then reconsider y = [**(cos (((2 * PI ) * 1) / n)),(sin (((2 * PI ) * 1) / n))**] as Element of (MultGroup F_Complex ) by A1;
A2: ord y = n div (1 gcd n) by Th34;
1 gcd n = 1 by WSIERP_1:13;
hence ex x being Element of (MultGroup F_Complex ) st ord x = n by A2, NAT_2:6; :: thesis: verum