set cMGFC = the carrier of (MultGroup F_Complex);

consider s being non empty finite Subset of F_Complex such that

A1: s = { y where y is Element of the carrier of (MultGroup F_Complex) : ord y = 1 } and

A2: cyclotomic_poly 1 = poly_with_roots ((s,1) -bag) by Def5;

A3: 1 -roots_of_1 = { x where x is Element of the carrier of (MultGroup F_Complex) : ord x divides 1 } by Th35;

hence cyclotomic_poly 1 = <%(- (1_ F_Complex)),(1_ F_Complex)%> by A2, Lm4, Th46; :: thesis: verum

consider s being non empty finite Subset of F_Complex such that

A1: s = { y where y is Element of the carrier of (MultGroup F_Complex) : ord y = 1 } and

A2: cyclotomic_poly 1 = poly_with_roots ((s,1) -bag) by Def5;

A3: 1 -roots_of_1 = { x where x is Element of the carrier of (MultGroup F_Complex) : ord x divides 1 } by Th35;

now :: thesis: for x being object holds

( ( x in s implies x in 1 -roots_of_1 ) & ( x in 1 -roots_of_1 implies x in s ) )

then
s = 1 -roots_of_1
by TARSKI:2;( ( x in s implies x in 1 -roots_of_1 ) & ( x in 1 -roots_of_1 implies x in s ) )

let x be object ; :: thesis: ( ( x in s implies x in 1 -roots_of_1 ) & ( x in 1 -roots_of_1 implies x in s ) )

then consider x1 being Element of the carrier of (MultGroup F_Complex) such that

A4: x = x1 and

A5: ord x1 divides 1 by A3;

ord x1 = 1 by A5, WSIERP_1:15;

hence x in s by A1, A4; :: thesis: verum

end;hereby :: thesis: ( x in 1 -roots_of_1 implies x in s )

assume
x in 1 -roots_of_1
; :: thesis: x in sassume
x in s
; :: thesis: x in 1 -roots_of_1

then ex x1 being Element of the carrier of (MultGroup F_Complex) st

( x = x1 & ord x1 = 1 ) by A1;

hence x in 1 -roots_of_1 by A3; :: thesis: verum

end;then ex x1 being Element of the carrier of (MultGroup F_Complex) st

( x = x1 & ord x1 = 1 ) by A1;

hence x in 1 -roots_of_1 by A3; :: thesis: verum

then consider x1 being Element of the carrier of (MultGroup F_Complex) such that

A4: x = x1 and

A5: ord x1 divides 1 by A3;

ord x1 = 1 by A5, WSIERP_1:15;

hence x in s by A1, A4; :: thesis: verum

hence cyclotomic_poly 1 = <%(- (1_ F_Complex)),(1_ F_Complex)%> by A2, Lm4, Th46; :: thesis: verum