set MGFC = MultGroup F_Complex ;
set cMGFC = the carrier of (MultGroup F_Complex );
set FC = F_Complex ;
let n be non empty 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 Th35;
( 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:103, ZFMISC_1:119;
hence n -th_roots_of_1 is Subgroup of MultGroup F_Complex by A2, GROUP_2:def 5; :: thesis: verum