set FC = F_Complex ;
set cFC = the carrier of F_Complex ;
set cMGFC = the carrier of (MultGroup F_Complex );
let n be non empty Element of NAT ; :: thesis: n -roots_of_1 c= the carrier of (MultGroup F_Complex )
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in n -roots_of_1 or a in the carrier of (MultGroup F_Complex ) )
assume a in n -roots_of_1 ; :: thesis: a in the carrier of (MultGroup F_Complex )
then consider x being Element of F_Complex such that
A1: a = x and
A2: x is CRoot of n, 1_ F_Complex ;
(power F_Complex ) . x,n = 1_ F_Complex by A2, COMPLFLD:def 2;
then A3: x <> 0. F_Complex by VECTSP_1:95;
A4: the carrier of (MultGroup F_Complex ) = the carrier of F_Complex \ {(0. F_Complex )} by Def1;
not x in {(0. F_Complex )} by A3, TARSKI:def 1;
hence a in the carrier of (MultGroup F_Complex ) by A1, A4, XBOOLE_0:def 5; :: thesis: verum