set mru = the multF of F_Complex || (n -roots_of_1 );
set X = [:(n -roots_of_1 ),(n -roots_of_1 ):];
A1: multcomplex = the multF of F_Complex by COMPLFLD:def 1;
n -roots_of_1 c= the carrier of F_Complex ;
then n -roots_of_1 c= COMPLEX by COMPLFLD:def 1;
then [:(n -roots_of_1 ),(n -roots_of_1 ):] c= [:COMPLEX ,COMPLEX :] by ZFMISC_1:119;
then A2: [:(n -roots_of_1 ),(n -roots_of_1 ):] c= dom multcomplex by FUNCT_2:def 1;
B3: dom (the multF of F_Complex || (n -roots_of_1 )) = (dom multcomplex ) /\ [:(n -roots_of_1 ),(n -roots_of_1 ):] by A1, RELAT_1:90;
then A3: dom (the multF of F_Complex || (n -roots_of_1 )) = [:(n -roots_of_1 ),(n -roots_of_1 ):] by A2, XBOOLE_1:28;
for x being set st x in [:(n -roots_of_1 ),(n -roots_of_1 ):] holds
(the multF of F_Complex || (n -roots_of_1 )) . x in n -roots_of_1

proof

let x be set ; :: thesis:
assume A4: x in [:(n -roots_of_1 ),(n -roots_of_1 ):] ; :: thesis:
consider a, b being set such that
A5: [a,b] = x by A4, RELAT_1:def 1;
A6: ( a in n -roots_of_1 & b in n -roots_of_1 ) by A4, A5, ZFMISC_1:106;
then reconsider a = a as Element of COMPLEX by COMPLFLD:def 1;
reconsider b = b as Element of COMPLEX by A6, COMPLFLD:def 1;
A7: multcomplex . a,b = a * b by BINOP_2:def 5;
(the multF of F_Complex || (n -roots_of_1 )) . [a,b] = multcomplex . [a,b] by A1, A3, A4, A5, FUNCT_1:70;
hence (the multF of F_Complex || (n -roots_of_1 )) . x in n -roots_of_1 by A5, A6, A7, Th28; :: thesis:

end;

then reconsider uM = the multF of F_Complex || (n -roots_of_1 ) as BinOp of n -roots_of_1 by B3, FUNCT_2:5, A2, XBOOLE_1:28;
A8: rng uM c= n -roots_of_1 by RELSET_1:12;
set H = multMagma(# (n -roots_of_1 ),uM #);
A9: for r, s, t being Element of multMagma(# (n -roots_of_1 ),uM #) holds (r * s) * t = r * (s * t)

proof

let r, s, t be Element of multMagma(# (n -roots_of_1 ),uM #); :: thesis:
( r in the carrier of F_Complex & s in the carrier of F_Complex & t in the carrier of F_Complex ) by TARSKI:def 3;
then A10: ( r is Element of COMPLEX & s is Element of COMPLEX & t is Element of COMPLEX ) by COMPLFLD:def 1;
set mc = multcomplex ;
A11: ( [r,s] in dom (the multF of F_Complex || (n -roots_of_1 )) & [s,t] in dom (the multF of F_Complex || (n -roots_of_1 )) ) by A3, ZFMISC_1:106;
then A12: ( (the multF of F_Complex || (n -roots_of_1 )) . [r,s] = multcomplex . [r,s] & (the multF of F_Complex || (n -roots_of_1 )) . [s,t] = multcomplex . [s,t] ) by A1, FUNCT_1:70;
(the multF of F_Complex || (n -roots_of_1 )) . [s,t] in rng (the multF of F_Complex || (n -roots_of_1 )) by A11, FUNCT_1:12;
then [r,((the multF of F_Complex || (n -roots_of_1 )) . [s,t])] in dom (the multF of F_Complex || (n -roots_of_1 )) by A3, A8, ZFMISC_1:106;
then A13: (the multF of F_Complex || (n -roots_of_1 )) . [r,((the multF of F_Complex || (n -roots_of_1 )) . [s,t])] = multcomplex . r,(multcomplex . s,t) by A1, A12, FUNCT_1:70;
(the multF of F_Complex || (n -roots_of_1 )) . [r,s] in rng (the multF of F_Complex || (n -roots_of_1 )) by A11, FUNCT_1:12;
then [((the multF of F_Complex || (n -roots_of_1 )) . [r,s]),t] in dom (the multF of F_Complex || (n -roots_of_1 )) by A3, A8, ZFMISC_1:106;
then (the multF of F_Complex || (n -roots_of_1 )) . [((the multF of F_Complex || (n -roots_of_1 )) . [r,s]),t] = multcomplex . (multcomplex . r,s),t by A1, A12, FUNCT_1:70;
hence (r * s) * t = r * (s * t) by A10, A13, BINOP_1:def 3; :: thesis:

end;

reconsider 1F = 1_ F_Complex as Element of multMagma(# (n -roots_of_1 ),uM #) by Th25;
A14: 1_ F_Complex = [**(cos (((2 * PI ) * 0 ) / n)),(sin (((2 * PI ) * 0 ) / n))**] by COMPLFLD:10, SIN_COS:34;
for s1 being Element of multMagma(# (n -roots_of_1 ),uM #) holds
( s1 * 1F = s1 & 1F * s1 = s1 & ex s2 being Element of multMagma(# (n -roots_of_1 ),uM #) st
( s1 * s2 = 1_ F_Complex & s2 * s1 = 1_ F_Complex ) )

proof

let s1 be Element of multMagma(# (n -roots_of_1 ),uM #); :: thesis:
A15: ( s1 * 1F = s1 & 1F * s1 = s1 )

proof

reconsider e1 = s1 as Element of F_Complex by TARSKI:def 3;
consider k being Element of NAT such that
A16: e1 = [**(cos (((2 * PI ) * k) / n)),(sin (((2 * PI ) * k) / n))**] by Th27;
A17: e1 * (1_ F_Complex ) = [**(cos (((2 * PI ) * ((k + 0 ) mod n)) / n)),(sin (((2 * PI ) * ((k + 0 ) mod n)) / n))**] by A14, A16, Th13
.= s1 by A16, Th12 ;
A18: (1_ F_Complex ) * e1 = [**(cos (((2 * PI ) * ((k + 0 ) mod n)) / n)),(sin (((2 * PI ) * ((k + 0 ) mod n)) / n))**] by A14, A16, Th13
.= s1 by A16, Th12 ;
A19: [s1,1F] in dom (the multF of F_Complex || (n -roots_of_1 )) by A3, ZFMISC_1:106;
[1F,s1] in dom (the multF of F_Complex || (n -roots_of_1 )) by A3, ZFMISC_1:106;
hence ( s1 * 1F = s1 & 1F * s1 = s1 ) by A17, A18, A19, FUNCT_1:70; :: thesis:

end;

ex s2 being Element of multMagma(# (n -roots_of_1 ),uM #) st
( s1 * s2 = 1_ F_Complex & s2 * s1 = 1_ F_Complex )

proof

s1 in the carrier of F_Complex by TARSKI:def 3;
then consider k being Element of NAT such that
A20: s1 = [**(cos (((2 * PI ) * k) / n)),(sin (((2 * PI ) * k) / n))**] by Th27;
reconsider e1 = [**(cos (((2 * PI ) * k) / n)),(sin (((2 * PI ) * k) / n))**] as Element of F_Complex ;
ex j being Element of NAT st (k + j) mod n = 0

proof

set r = k mod n;
A21: k = (n * (k div n)) + (k mod n) by NAT_D:2;
k mod n < n by NAT_D:1;
then consider j being Nat such that
A22: (k mod n) + j = n by NAT_1:10;
A23: j in NAT by ORDINAL1:def 13;
(k + j) mod n = (((k div n) + 1) * n) mod n by A21, A22;
hence ex j being Element of NAT st (k + j) mod n = 0 by A23, NAT_D:13; :: thesis:

end;

then consider j being Element of NAT such that
A24: (k + j) mod n = 0 ;
set ss2 = [**(cos (((2 * PI ) * j) / n)),(sin (((2 * PI ) * j) / n))**];
reconsider s2 = [**(cos (((2 * PI ) * j) / n)),(sin (((2 * PI ) * j) / n))**] as Element of multMagma(# (n -roots_of_1 ),uM #) by Th27;
reconsider e2 = s2 as Element of F_Complex ;
A25: e1 * e2 = [**(cos (((2 * PI ) * ((j + k) mod n)) / n)),(sin (((2 * PI ) * ((j + k) mod n)) / n))**] by Th13;
[s1,s2] in dom (the multF of F_Complex || (n -roots_of_1 )) by A3, ZFMISC_1:106;
then A26: s1 * s2 = 1_ F_Complex by A20, A24, A25, COMPLFLD:10, FUNCT_1:70, SIN_COS:34;
A27: e2 * e1 = [**(cos (((2 * PI ) * ((j + k) mod n)) / n)),(sin (((2 * PI ) * ((j + k) mod n)) / n))**] by Th13;
[s2,s1] in dom (the multF of F_Complex || (n -roots_of_1 )) by A3, ZFMISC_1:106;
then s2 * s1 = 1_ F_Complex by A20, A24, A27, COMPLFLD:10, FUNCT_1:70, SIN_COS:34;
hence ex s2 being Element of multMagma(# (n -roots_of_1 ),uM #) st
( s1 * s2 = 1_ F_Complex & s2 * s1 = 1_ F_Complex ) by A26; :: thesis:

end;

hence ( s1 * 1F = s1 & 1F * s1 = s1 & ex s2 being Element of multMagma(# (n -roots_of_1 ),uM #) st
( s1 * s2 = 1_ F_Complex & s2 * s1 = 1_ F_Complex ) ) by A15; :: thesis:

end;

then multMagma(# (n -roots_of_1 ),uM #) is Group by A9, GROUP_1:5;
hence ex b₁ being strict Group st
( the carrier of b₁ = n -roots_of_1 & the multF of b₁ = the multF of F_Complex || (n -roots_of_1 ) ) ; :: thesis: