set MGFC = MultGroup F_Complex ;
set cMGFC = the carrier of (MultGroup F_Complex );
let n be non empty 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 Th35;

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, Th37;
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 Th37; :: thesis: verum