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 )

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

thus
( x is CRoot of n, 1_ F_Complex implies x in n -roots_of_1 )
; :: thesis: verumassume
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;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