set cMGFC = the carrier of (MultGroup F_Complex);

reconsider d = d as non zero Element of NAT by ORDINAL1:def 12;

defpred S_{1}[ 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_{1}[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

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) : S_{1}[y] } c= d -roots_of_1

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) : S_{1}[y] }
;

then reconsider s = { y where y is Element of the carrier of (MultGroup F_Complex) : S_{1}[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

reconsider d = d as non zero Element of NAT by ORDINAL1:def 12;

defpred S

set s = { y where y is Element of the carrier of (MultGroup F_Complex) : S

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

then A2:
not [**(cos (((2 * PI) * 1) / d)),(sin (((2 * PI) * 1) / d))**] in {(0. F_Complex)}
by TARSKI:def 1;
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 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

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) : S

proof

1 gcd i = 1
by WSIERP_1:8;
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) : S_{1}[y] } or a in d -roots_of_1 )

assume a in { y where y is Element of the carrier of (MultGroup F_Complex) : S_{1}[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;assume a in { y where y is Element of the carrier of (MultGroup F_Complex) : S

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

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) : S

then reconsider s = { y where y is Element of the carrier of (MultGroup F_Complex) : S

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