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;

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 } ) )

hence
n -roots_of_1 = { x where x is Element of (MultGroup F_Complex) : ord x divides n }
by TARSKI:2; :: thesis: verum( ( 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 } ) )

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;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
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 } 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;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

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