let n be non empty Element of NAT ; :: thesis: n -roots_of_1 c= the carrier of (MultGroup F_Complex )
set cMGFC = the carrier of (MultGroup F_Complex );
set cFC = the carrier of F_Complex ;
set FC = 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 x <> 0. F_Complex by VECTSP_1:95;
then A3: not x in {(0. F_Complex )} by TARSKI:def 1;
the carrier of (MultGroup F_Complex ) = NonZero F_Complex by Def1;
hence a in the carrier of (MultGroup F_Complex ) by A1, A3, XBOOLE_0:def 5; :: thesis: verum