set X = [:(n -roots_of_1 ),(n -roots_of_1 ):];
set mru = the multF of F_Complex || (n -roots_of_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 A1: [:(n -roots_of_1 ),(n -roots_of_1 ):] c= dom multcomplex by FUNCT_2:def 1;
A2: multcomplex = the multF of F_Complex by COMPLFLD:def 1;
then A3: dom (the multF of F_Complex || (n -roots_of_1 )) = (dom multcomplex ) /\ [:(n -roots_of_1 ),(n -roots_of_1 ):] by RELAT_1:90;
then A4: dom (the multF of F_Complex || (n -roots_of_1 )) = [:(n -roots_of_1 ),(n -roots_of_1 ):] by A1, 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: ( x in [:(n -roots_of_1 ),(n -roots_of_1 ):] implies (the multF of F_Complex || (n -roots_of_1 )) . x in n -roots_of_1 )
assume A5: x in [:(n -roots_of_1 ),(n -roots_of_1 ):] ; :: thesis: (the multF of F_Complex || (n -roots_of_1 )) . x in n -roots_of_1
consider a, b being set such that
A6: [a,b] = x by A5, RELAT_1:def 1;
A7: b in n -roots_of_1 by A5, A6, ZFMISC_1:106;
A8: a in n -roots_of_1 by A5, A6, ZFMISC_1:106;
reconsider b = b as Element of COMPLEX by A7, COMPLFLD:def 1;
reconsider a = a as Element of COMPLEX by A8, COMPLFLD:def 1;
( multcomplex . a,b = a * b & (the multF of F_Complex || (n -roots_of_1 )) . [a,b] = multcomplex . [a,b] ) by A2, A4, A5, A6, BINOP_2:def 5, FUNCT_1:70;
hence (the multF of F_Complex || (n -roots_of_1 )) . x in n -roots_of_1 by A6, A8, A7, Th28; :: thesis: verum

end;

then reconsider uM = the multF of F_Complex || (n -roots_of_1 ) as BinOp of (n -roots_of_1 ) by A1, A3, FUNCT_2:5, XBOOLE_1:28;
set H = multMagma(# (n -roots_of_1 ),uM #);
reconsider 1F = 1_ F_Complex as Element of multMagma(# (n -roots_of_1 ),uM #) by Th25;
A9: 1_ F_Complex = [**(cos (((2 * PI ) * 0 ) / n)),(sin (((2 * PI ) * 0 ) / n))**] by COMPLFLD:10, SIN_COS:34;
A10: 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: ( 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 ) )
A11: 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
A12: 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;
k mod n < n by NAT_D:1;
then consider j being Nat such that
A13: (k mod n) + j = n by NAT_1:10;
k = (n * (k div n)) + (k mod n) by NAT_D:2;
then ( j in NAT & (k + j) mod n = (((k div n) + 1) * n) mod n ) by A13, ORDINAL1:def 13;
hence ex j being Element of NAT st (k + j) mod n = 0 by NAT_D:13; :: thesis: verum

end;

then consider j being Element of NAT such that
A14: (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 ;
( e2 * e1 = [**(cos (((2 * PI ) * ((j + k) mod n)) / n)),(sin (((2 * PI ) * ((j + k) mod n)) / n))**] & [s2,s1] in dom (the multF of F_Complex || (n -roots_of_1 )) ) by A4, Th13, ZFMISC_1:106;
then A15: s2 * s1 = 1_ F_Complex by A12, A14, COMPLFLD:10, FUNCT_1:70, SIN_COS:34;
( e1 * e2 = [**(cos (((2 * PI ) * ((j + k) mod n)) / n)),(sin (((2 * PI ) * ((j + k) mod n)) / n))**] & [s1,s2] in dom (the multF of F_Complex || (n -roots_of_1 )) ) by A4, Th13, ZFMISC_1:106;
then s1 * s2 = 1_ F_Complex by A12, A14, 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 A15; :: thesis: verum

end;

( s1 * 1F = s1 & 1F * s1 = s1 )

proof

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

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 A11; :: thesis: verum

end;

A19: rng uM c= n -roots_of_1 by RELAT_1:def 19;
for r, s, t being Element of multMagma(# (n -roots_of_1 ),uM #) holds (r * s) * t = r * (s * t)

proof

set mc = multcomplex ;
let r, s, t be Element of multMagma(# (n -roots_of_1 ),uM #); :: thesis: (r * s) * t = r * (s * t)
r in the carrier of F_Complex by TARSKI:def 3;
then A20: r is Element of COMPLEX by COMPLFLD:def 1;
s in the carrier of F_Complex by TARSKI:def 3;
then A21: s is Element of COMPLEX by COMPLFLD:def 1;
A22: [r,s] in dom (the multF of F_Complex || (n -roots_of_1 )) by A4, ZFMISC_1:106;
then (the multF of F_Complex || (n -roots_of_1 )) . [r,s] in rng (the multF of F_Complex || (n -roots_of_1 )) by FUNCT_1:12;
then A23: [((the multF of F_Complex || (n -roots_of_1 )) . [r,s]),t] in dom (the multF of F_Complex || (n -roots_of_1 )) by A4, A19, ZFMISC_1:106;
A24: [s,t] in dom (the multF of F_Complex || (n -roots_of_1 )) by A4, ZFMISC_1:106;
then (the multF of F_Complex || (n -roots_of_1 )) . [s,t] in rng (the multF of F_Complex || (n -roots_of_1 )) by FUNCT_1:12;
then A25: [r,((the multF of F_Complex || (n -roots_of_1 )) . [s,t])] in dom (the multF of F_Complex || (n -roots_of_1 )) by A4, A19, ZFMISC_1:106;
(the multF of F_Complex || (n -roots_of_1 )) . [s,t] = multcomplex . [s,t] by A2, A24, FUNCT_1:70;
then A26: (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 A2, A25, FUNCT_1:70;
t in the carrier of F_Complex by TARSKI:def 3;
then A27: t is Element of COMPLEX by COMPLFLD:def 1;
(the multF of F_Complex || (n -roots_of_1 )) . [r,s] = multcomplex . [r,s] by A2, A22, FUNCT_1:70;
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 A2, A23, FUNCT_1:70;
hence (r * s) * t = r * (s * t) by A20, A21, A27, A26, BINOP_1:def 3; :: thesis: verum

end;

then multMagma(# (n -roots_of_1 ),uM #) is Group by A10, 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: verum