let n be non zero 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 ex y being Element of F_Complex st
( y = x & y is CRoot of n, 1_ F_Complex ) ;
hence x is CRoot of n, 1_ F_Complex ; :: thesis: verum

end;

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