let n be non empty Element of NAT ; :: thesis: card (n -roots_of_1 ) = n
set X = { [**(cos (((2 * PI ) * k) / n)),(sin (((2 * PI ) * k) / n))**] where k is Element of NAT : k < n } ;
A1: { [**(cos (((2 * PI ) * k) / n)),(sin (((2 * PI ) * k) / n))**] where k is Element of NAT : k < n } = n -roots_of_1 by Th29;
defpred S₁[ set , set ] means ex j being Element of NAT st
( j = $1 & $2 = [**(cos (((2 * PI ) * (j -' 1)) / n)),(sin (((2 * PI ) * (j -' 1)) / n))**] );
[**(cos (((2 * PI ) * 0 ) / n)),(sin (((2 * PI ) * 0 ) / n))**] in { [**(cos (((2 * PI ) * k) / n)),(sin (((2 * PI ) * k) / n))**] where k is Element of NAT : k < n } ;
then reconsider Y = { [**(cos (((2 * PI ) * k) / n)),(sin (((2 * PI ) * k) / n))**] where k is Element of NAT : k < n } as non empty set ;
A2: for x being set st x in Seg n holds
ex y being set st
( y in Y & S₁[x,y] )

proof

let x be set ; :: thesis: ( x in Seg n implies ex y being set st
( y in Y & S₁[x,y] ) )
assume A3: x in Seg n ; :: thesis: ex y being set st
( y in Y & S₁[x,y] )
reconsider a = x as Element of NAT by A3;
A4: ( 1 <= a & a <= n ) by A3, FINSEQ_1:3;
then a < n + 1 by NAT_1:13;
then a - 1 < (n + 1) - 1 by XREAL_1:16;
then A5: a -' 1 < n by A4, XREAL_1:235;
consider b being Element of NAT such that
A6: b = a -' 1 ;
[**(cos (((2 * PI ) * b) / n)),(sin (((2 * PI ) * b) / n))**] in { [**(cos (((2 * PI ) * k) / n)),(sin (((2 * PI ) * k) / n))**] where k is Element of NAT : k < n } by A5, A6;
hence ex y being set st
( y in Y & S₁[x,y] ) by A6; :: thesis: verum

end;

consider F being Function of (Seg n),Y such that
A7: for x being set st x in Seg n holds
S₁[x,F . x] from FUNCT_2:sch 1(A2);
A8: dom F = Seg n by FUNCT_2:def 1;
for c being set st c in { [**(cos (((2 * PI ) * k) / n)),(sin (((2 * PI ) * k) / n))**] where k is Element of NAT : k < n } holds
ex x being set st
( x in Seg n & c = F . x )

proof

let c be set ; :: thesis: ( c in { [**(cos (((2 * PI ) * k) / n)),(sin (((2 * PI ) * k) / n))**] where k is Element of NAT : k < n } implies ex x being set st
( x in Seg n & c = F . x ) )
assume A9: c in { [**(cos (((2 * PI ) * k) / n)),(sin (((2 * PI ) * k) / n))**] where k is Element of NAT : k < n } ; :: thesis: ex x being set st
( x in Seg n & c = F . x )
consider k being Element of NAT such that
A10: ( c = [**(cos (((2 * PI ) * k) / n)),(sin (((2 * PI ) * k) / n))**] & k < n ) by A9;
0 + 1 <= k + 1 by XREAL_1:9;
then ( 1 <= k + 1 & k + 1 <= n ) by A10, INT_1:20;
then A11: k + 1 in Seg n by FINSEQ_1:3;
then consider j being Element of NAT such that
A12: ( j = k + 1 & F . (k + 1) = [**(cos (((2 * PI ) * (j -' 1)) / n)),(sin (((2 * PI ) * (j -' 1)) / n))**] ) by A7;
(k + 1) -' 1 = k by NAT_D:34;
hence ex x being set st
( x in Seg n & c = F . x ) by A10, A11, A12; :: thesis: verum

end;

then A13: rng F = { [**(cos (((2 * PI ) * k) / n)),(sin (((2 * PI ) * k) / n))**] where k is Element of NAT : k < n } by FUNCT_2:16;
for x1, x2 being set st x1 in dom F & x2 in dom F & F . x1 = F . x2 holds
x1 = x2

proof

let x1, x2 be set ; :: thesis: ( x1 in dom F & x2 in dom F & F . x1 = F . x2 implies x1 = x2 )
assume A14: ( x1 in dom F & x2 in dom F & F . x1 = F . x2 ) ; :: thesis: x1 = x2
A15: ( x1 in Seg n & x2 in Seg n ) by A14, FUNCT_2:def 1;
then consider j being Element of NAT such that
A16: ( j = x1 & F . x1 = [**(cos (((2 * PI ) * (j -' 1)) / n)),(sin (((2 * PI ) * (j -' 1)) / n))**] ) by A7;
consider k being Element of NAT such that
A17: ( k = x2 & F . x2 = [**(cos (((2 * PI ) * (k -' 1)) / n)),(sin (((2 * PI ) * (k -' 1)) / n))**] ) by A7, A15;
A18: ( cos (((2 * PI ) * (j -' 1)) / n) = cos (((2 * PI ) * (k -' 1)) / n) & sin (((2 * PI ) * (j -' 1)) / n) = sin (((2 * PI ) * (k -' 1)) / n) ) by A14, A16, A17, COMPLEX1:163;
A19: ( 1 <= j & j <= n ) by A15, A16, FINSEQ_1:3;
A20: ( 1 <= k & k <= n ) by A15, A17, FINSEQ_1:3;
j - 1 < n by A19, XREAL_1:148, XXREAL_0:2;
then A21: j -' 1 < n by A19, XREAL_1:235;
k - 1 < n by A20, XREAL_1:148, XXREAL_0:2;
then A22: k -' 1 < n by A20, XREAL_1:235;
set a1 = ((2 * PI ) * (j -' 1)) / n;
set a2 = ((2 * PI ) * (k -' 1)) / n;
(j -' 1) / n < n / n by A21, XREAL_1:76;
then (j -' 1) / n < 1 by XCMPLX_1:60;
then ((j -' 1) / n) * (2 * PI ) < 1 * (2 * PI ) by COMPTRIG:21, XREAL_1:70;
then A24: ( 0 <= ((2 * PI ) * (j -' 1)) / n & ((2 * PI ) * (j -' 1)) / n < 2 * PI ) by COMPTRIG:21, XCMPLX_1:75;
(k -' 1) / n < n / n by A22, XREAL_1:76;
then (k -' 1) / n < 1 by XCMPLX_1:60;
then ((k -' 1) / n) * (2 * PI ) < 1 * (2 * PI ) by COMPTRIG:21, XREAL_1:70;
then ( 0 <= ((2 * PI ) * (k -' 1)) / n & ((2 * PI ) * (k -' 1)) / n < 2 * PI ) by COMPTRIG:21, XCMPLX_1:75;
then ((2 * PI ) * (j -' 1)) / n = ((2 * PI ) * (k -' 1)) / n by A18, A24, COMPLEX2:12;
then (((2 * PI ) * (j -' 1)) / n) * n = (2 * PI ) * (k -' 1) by XCMPLX_1:88;
then j -' 1 = k -' 1 by COMPTRIG:21, XCMPLX_1:5, XCMPLX_1:88;
then j = (k -' 1) + 1 by A19, XREAL_1:237;
hence x1 = x2 by A16, A17, A20, XREAL_1:237; :: thesis: verum

end;

then F is one-to-one by FUNCT_1:def 8;
then Seg n,F .: (Seg n) are_equipotent by A8, CARD_1:60;
then Seg n, rng F are_equipotent by A8, RELAT_1:146;
then card (Seg n) = card { [**(cos (((2 * PI ) * k) / n)),(sin (((2 * PI ) * k) / n))**] where k is Element of NAT : k < n } by A13, CARD_1:21;
hence card (n -roots_of_1 ) = n by A1, FINSEQ_1:78; :: thesis: verum