set cMGFC = the carrier of (MultGroup F_Complex );
reconsider d = d as non empty Element of NAT by ORDINAL1:def 13;
defpred S₁[ 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 ) : S₁[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:9;
then cos (((2 * PI ) * 1) / d) = 0 by COMPLEX1:163;
hence contradiction by A1, COMPLEX2:11, COMPLFLD:9; :: 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 Th38;
A4: { y where y is Element of the carrier of (MultGroup F_Complex ) : S₁[y] } c= d -roots_of_1

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { y where y is Element of the carrier of (MultGroup F_Complex ) : S₁[y] } or a in d -roots_of_1 )
assume a in { y where y is Element of the carrier of (MultGroup F_Complex ) : S₁[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:13;
then ord x = d div 1 by Th34
.= d by NAT_2:6 ;
then x in { y where y is Element of the carrier of (MultGroup F_Complex ) : S₁[y] } ;
then reconsider s = { y where y is Element of the carrier of (MultGroup F_Complex ) : S₁[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