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

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