set X = [:(),():];
set mru = the multF of F_Complex || ();
n -roots_of_1 c= the carrier of F_Complex ;
then n -roots_of_1 c= COMPLEX by COMPLFLD:def 1;
then [:(),():] c= by ZFMISC_1:96;
then A1: [:(),():] 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 || ()) = /\ [:(),():] by RELAT_1:61;
then A4: dom ( the multF of F_Complex || ()) = [:(),():] by ;
for x being object st x in [:(),():] holds
( the multF of F_Complex || ()) . x in n -roots_of_1
proof
let x be object ; :: thesis: ( x in [:(),():] implies ( the multF of F_Complex || ()) . x in n -roots_of_1 )
assume A5: x in [:(),():] ; :: thesis: ( the multF of F_Complex || ()) . x in n -roots_of_1
consider a, b being object such that
A6: [a,b] = x by ;
A7: b in n -roots_of_1 by ;
A8: a in n -roots_of_1 by ;
reconsider b = b as Element of COMPLEX by ;
reconsider a = a as Element of COMPLEX by ;
( multcomplex . (a,b) = a * b & ( the multF of F_Complex || ()) . [a,b] = multcomplex . [a,b] ) by ;
hence ( the multF of F_Complex || ()) . x in n -roots_of_1 by A6, A8, A7, Th25; :: thesis: verum
end;
then reconsider uM = the multF of F_Complex || () as BinOp of () by ;
set H = multMagma(# (),uM #);
reconsider 1F = 1_ F_Complex as Element of multMagma(# (),uM #) by Th22;
A9: 1_ F_Complex = [**(cos (((2 * PI) * 0) / n)),(sin (((2 * PI) * 0) / n))**] by ;
A10: for s1 being Element of multMagma(# (),uM #) holds
( s1 * 1F = s1 & 1F * s1 = s1 & ex s2 being Element of multMagma(# (),uM #) st
( s1 * s2 = 1_ F_Complex & s2 * s1 = 1_ F_Complex ) )
proof
let s1 be Element of multMagma(# (),uM #); :: thesis: ( s1 * 1F = s1 & 1F * s1 = s1 & ex s2 being Element of multMagma(# (),uM #) st
( s1 * s2 = 1_ F_Complex & s2 * s1 = 1_ F_Complex ) )

A11: ex s2 being Element of multMagma(# (),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 Th24;
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 ;
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(# (),uM #) by Th24;
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 || ()) ) by ;
then A15: s2 * s1 = 1_ F_Complex by ;
( 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 || ()) ) by ;
then s1 * s2 = 1_ F_Complex by ;
hence ex s2 being Element of multMagma(# (),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 || ()) & [1F,s1] in dom ( the multF of F_Complex || ()) ) by ;
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 Th24;
A18: () * e1 = [**(cos (((2 * PI) * ((k + 0) mod n)) / n)),(sin (((2 * PI) * ((k + 0) mod n)) / n))**] by
.= s1 by ;
e1 * () = [**(cos (((2 * PI) * ((k + 0) mod n)) / n)),(sin (((2 * PI) * ((k + 0) mod n)) / n))**] by
.= s1 by ;
hence ( s1 * 1F = s1 & 1F * s1 = s1 ) by ; :: thesis: verum
end;
hence ( s1 * 1F = s1 & 1F * s1 = s1 & ex s2 being Element of multMagma(# (),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(# (),uM #) holds (r * s) * t = r * (s * t)
proof
set mc = multcomplex ;
let r, s, t be Element of multMagma(# (),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 || ()) by ;
then ( the multF of F_Complex || ()) . [r,s] in rng ( the multF of F_Complex || ()) by FUNCT_1:3;
then A23: [(( the multF of F_Complex || ()) . [r,s]),t] in dom ( the multF of F_Complex || ()) by ;
A24: [s,t] in dom ( the multF of F_Complex || ()) by ;
then ( the multF of F_Complex || ()) . [s,t] in rng ( the multF of F_Complex || ()) by FUNCT_1:3;
then A25: [r,(( the multF of F_Complex || ()) . [s,t])] in dom ( the multF of F_Complex || ()) by ;
( the multF of F_Complex || ()) . [s,t] = multcomplex . [s,t] by ;
then A26: ( the multF of F_Complex || ()) . [r,(( the multF of F_Complex || ()) . [s,t])] = multcomplex . (r,(multcomplex . (s,t))) by ;
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 || ()) . [r,s] = multcomplex . [r,s] by ;
then ( the multF of F_Complex || ()) . [(( the multF of F_Complex || ()) . [r,s]),t] = multcomplex . ((multcomplex . (r,s)),t) by ;
hence (r * s) * t = r * (s * t) by ; :: thesis: verum
end;
then multMagma(# (),uM #) is Group by ;
hence ex b1 being strict Group st
( the carrier of b1 = n -roots_of_1 & the multF of b1 = the multF of F_Complex || () ) ; :: thesis: verum