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

now

let a be set ; :: 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, Th37;
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, Th37; :: 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