set cMGFC = the carrier of (MultGroup F_Complex);
set MGFC = MultGroup F_Complex;
let n be non zero Element of NAT ; :: thesis:
set R = { a where a is Element of F_Complex : a is CRoot of n, 1_ F_Complex } ;
set S = { x where x is Element of (MultGroup F_Complex) : ord x divides n } ;
A1: n -roots_of_1 = { a where a is Element of F_Complex : a is CRoot of n, 1_ F_Complex } ;
then A2: { a where a is Element of F_Complex : a is CRoot of n, 1_ F_Complex } c= the carrier of (MultGroup F_Complex) by Th32;

now :: thesis:

let a be object ; :: thesis:

hereby :: thesis:

assume A3: a in { a where a is Element of F_Complex : a is CRoot of n, 1_ F_Complex } ; :: thesis:
then reconsider x = a as Element of (MultGroup F_Complex) by A2;
ord x divides n by A1, A3, Th34;
hence a in { x where x is Element of (MultGroup F_Complex) : ord x divides n } ; :: thesis:

end;

assume a in { x where x is Element of (MultGroup F_Complex) : ord x divides n } ; :: thesis:
then ex x being Element of (MultGroup F_Complex) st
( a = x & ord x divides n ) ;
hence a in { a where a is Element of F_Complex : a is CRoot of n, 1_ F_Complex } by A1, Th34; :: thesis:

end;

hence n -roots_of_1 = { x where x is Element of (MultGroup F_Complex) : ord x divides n } by TARSKI:2; :: thesis: