set cMGFC = the carrier of (MultGroup F_Complex);
reconsider d = d as non zero Element of NAT by ORDINAL1:def 12;
defpred S1[ Element of the carrier of (MultGroup F_Complex)] means ord $1 = d;
set s = { y where y is Element of the carrier of (MultGroup F_Complex) : S1[y] } ;
set x = [**(cos (((2 * PI) * 1) / d)),(sin (((2 * PI) * 1) / d))**];
reconsider i = d as Integer ;
[**(cos (((2 * PI) * 1) / d)),(sin (((2 * PI) * 1) / d))**] <> 0. F_Complex
proof
assume A1: [**(cos (((2 * PI) * 1) / d)),(sin (((2 * PI) * 1) / d))**] = 0. F_Complex ; :: thesis: contradiction
then 0 + (0 * <i>) = (cos (((2 * PI) * 1) / d)) + ((sin (((2 * PI) * 1) / d)) * <i>) by COMPLFLD:7;
then cos (((2 * PI) * 1) / d) = 0 by COMPLEX1:77;
hence contradiction by A1, COMPLEX2:10, COMPLFLD:7; :: thesis: verum
end;
then A2: not [**(cos (((2 * PI) * 1) / d)),(sin (((2 * PI) * 1) / d))**] in {(0. F_Complex)} by TARSKI:def 1;
the carrier of (MultGroup F_Complex) = NonZero F_Complex by Def1;
then reconsider x = [**(cos (((2 * PI) * 1) / d)),(sin (((2 * PI) * 1) / d))**] as Element of the carrier of (MultGroup F_Complex) by A2, XBOOLE_0:def 5;
A3: d -roots_of_1 = { y where y is Element of the carrier of (MultGroup F_Complex) : ord y divides d } by Th35;
A4: { y where y is Element of the carrier of (MultGroup F_Complex) : S1[y] } c= d -roots_of_1
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { y where y is Element of the carrier of (MultGroup F_Complex) : S1[y] } or a in d -roots_of_1 )
assume a in { y where y is Element of the carrier of (MultGroup F_Complex) : S1[y] } ; :: thesis: a in d -roots_of_1
then ex y being Element of the carrier of (MultGroup F_Complex) st
( a = y & ord y = d ) ;
hence a in d -roots_of_1 by A3; :: thesis: verum
end;
1 gcd i = 1 by WSIERP_1:8;
then ord x = d div 1 by Th31
.= d by NAT_2:4 ;
then x in { y where y is Element of the carrier of (MultGroup F_Complex) : S1[y] } ;
then reconsider s = { y where y is Element of the carrier of (MultGroup F_Complex) : S1[y] } as non empty finite Subset of F_Complex by A4, XBOOLE_1:1;
take poly_with_roots ((s,1) -bag) ; :: thesis: ex s being non empty finite Subset of F_Complex st
( s = { y where y is Element of (MultGroup F_Complex) : ord y = d } & poly_with_roots ((s,1) -bag) = poly_with_roots ((s,1) -bag) )
thus ex s being non empty finite Subset of F_Complex st
( s = { y where y is Element of (MultGroup F_Complex) : ord y = d } & poly_with_roots ((s,1) -bag) = poly_with_roots ((s,1) -bag) ) ; :: thesis: verum