set cMGFC = the carrier of (MultGroup F_Complex);
set MGFC = MultGroup F_Complex;
let n be non zero Element of NAT ; :: thesis: n -roots_of_1 = { x where x is Element of (MultGroup F_Complex) : ord x divides n }
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: for a being object holds
( ( a in { a where a is Element of F_Complex : a is CRoot of n, 1_ F_Complex } implies a in { x where x is Element of (MultGroup F_Complex) : ord x divides n } ) & ( a in { x where x is Element of (MultGroup F_Complex) : ord x divides n } implies a in { a where a is Element of F_Complex : a is CRoot of n, 1_ F_Complex } ) )

let a be object ; :: thesis: ( ( a in { a where a is Element of F_Complex : a is CRoot of n, 1_ F_Complex } implies a in { x where x is Element of (MultGroup F_Complex) : ord x divides n } ) & ( a in { x where x is Element of (MultGroup F_Complex) : ord x divides n } implies a in { a where a is Element of F_Complex : a is CRoot of n, 1_ F_Complex } ) )

hereby :: thesis: ( a in { x where x is Element of (MultGroup F_Complex) : ord x divides n } implies a in { a where a is Element of F_Complex : a is CRoot of n, 1_ F_Complex } )

assume A3: a in { a where a is Element of F_Complex : a is CRoot of n, 1_ F_Complex } ; :: thesis: a in { x where x is Element of (MultGroup F_Complex) : ord x divides n }
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: verum

end;

assume a in { x where x is Element of (MultGroup F_Complex) : ord x divides n } ; :: thesis: a in { a where a is Element of F_Complex : a is CRoot of n, 1_ F_Complex }
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: verum

end;

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