set MGFC = MultGroup F_Complex;

set cMGFC = the carrier of (MultGroup F_Complex);

set FC = F_Complex ;

let n be non zero Element of NAT ; :: thesis: n -th_roots_of_1 is Subgroup of MultGroup F_Complex

set nth = n -th_roots_of_1 ;

set cnth = the carrier of (n -th_roots_of_1);

A1: the carrier of (n -th_roots_of_1) = n -roots_of_1 by Def3;

then A2: the carrier of (n -th_roots_of_1) c= the carrier of (MultGroup F_Complex) by Th32;

( the multF of (n -th_roots_of_1) = the multF of F_Complex || (n -roots_of_1) & the multF of (MultGroup F_Complex) = the multF of F_Complex || the carrier of (MultGroup F_Complex) ) by Def1, Def3;

then the multF of (n -th_roots_of_1) = the multF of (MultGroup F_Complex) || the carrier of (n -th_roots_of_1) by A1, A2, RELAT_1:74, ZFMISC_1:96;

hence n -th_roots_of_1 is Subgroup of MultGroup F_Complex by A2, GROUP_2:def 5; :: thesis: verum

set cMGFC = the carrier of (MultGroup F_Complex);

set FC = F_Complex ;

let n be non zero Element of NAT ; :: thesis: n -th_roots_of_1 is Subgroup of MultGroup F_Complex

set nth = n -th_roots_of_1 ;

set cnth = the carrier of (n -th_roots_of_1);

A1: the carrier of (n -th_roots_of_1) = n -roots_of_1 by Def3;

then A2: the carrier of (n -th_roots_of_1) c= the carrier of (MultGroup F_Complex) by Th32;

( the multF of (n -th_roots_of_1) = the multF of F_Complex || (n -roots_of_1) & the multF of (MultGroup F_Complex) = the multF of F_Complex || the carrier of (MultGroup F_Complex) ) by Def1, Def3;

then the multF of (n -th_roots_of_1) = the multF of (MultGroup F_Complex) || the carrier of (n -th_roots_of_1) by A1, A2, RELAT_1:74, ZFMISC_1:96;

hence n -th_roots_of_1 is Subgroup of MultGroup F_Complex by A2, GROUP_2:def 5; :: thesis: verum