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