let n be non zero Element of NAT ; :: thesis: n -roots_of_1 c= the carrier of (MultGroup F_Complex)
set cMGFC = the carrier of (MultGroup F_Complex);
set FC = F_Complex ;
let a be object ; :: 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:36;
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