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;

( x = y & ord y divides n ) implies x in n -roots_of_1 ) by Th34; :: thesis: verum

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 )

thus
( 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;( 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

( x = y & ord y divides n ) implies x in n -roots_of_1 ) by Th34; :: thesis: verum