let n be non empty Element of NAT ; :: thesis: for x being Element of F_Complex holds
( x in n -roots_of_1 iff x is CRoot of n, 1_ F_Complex )
let x be Element of F_Complex ; :: thesis: ( x in n -roots_of_1 iff x is CRoot of n, 1_ F_Complex )

hereby :: thesis: ( x is CRoot of n, 1_ F_Complex implies x in n -roots_of_1 )

assume x in n -roots_of_1 ; :: thesis: x is CRoot of n, 1_ F_Complex
then consider y being Element of F_Complex such that
A1: y = x and
A2: y is CRoot of n, 1_ F_Complex ;
thus x is CRoot of n, 1_ F_Complex by A1, A2; :: thesis: verum

end;

thus ( x is CRoot of n, 1_ F_Complex implies x in n -roots_of_1 ) ; :: thesis: verum