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;
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 ) )
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 ) )
hereby :: thesis: ( x in 1 -roots_of_1 implies x in s )
assume 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;
assume x in 1 -roots_of_1 ; :: thesis: 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;
then s = 1 -roots_of_1 by TARSKI:2;
hence cyclotomic_poly 1 = <%(- (1_ F_Complex)),(1_ F_Complex)%> by A2, Lm4, Th46; :: thesis: verum