set MGFC = MultGroup F_Complex;
set cMGFC = the carrier of (MultGroup F_Complex);
let n be non zero Element of NAT ; :: thesis: for x being set holds
( x in n -roots_of_1 iff ex y being Element of (MultGroup F_Complex) st
( x = y & ord y divides n ) )
let x be set ; :: thesis: ( x in n -roots_of_1 iff ex y being Element of (MultGroup F_Complex) st
( x = y & ord y divides n ) )
A1: n -roots_of_1 c= the carrier of (MultGroup F_Complex) by Th32;

hereby :: thesis: ( ex y being Element of (MultGroup F_Complex) st
( x = y & ord y divides n ) implies x in n -roots_of_1 )

assume A2: x in n -roots_of_1 ; :: thesis: ex y being Element of (MultGroup F_Complex) st
( x = y & ord y divides n )
then reconsider a = x as Element of (MultGroup F_Complex) by A1;
ord a divides n by A2, Th34;
hence ex y being Element of (MultGroup F_Complex) st
( x = y & ord y divides n ) ; :: thesis: verum

end;

thus ( ex y being Element of (MultGroup F_Complex) st
( x = y & ord y divides n ) implies x in n -roots_of_1 ) by Th34; :: thesis: verum