let n be non zero 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 } ;
defpred S₁[ object , object ] means ex j being Element of NAT st
( j = $1 & $2 = [**(cos (((2 * PI) * (j -' 1)) / n)),(sin (((2 * PI) * (j -' 1)) / 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 Th26;
[**(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 object st x in Seg n holds
ex y being object st
( y in Y & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in Seg n implies ex y being object st
( y in Y & S₁[x,y] ) )
assume A3: x in Seg n ; :: thesis: ex y being object st
( y in Y & S₁[x,y] )
reconsider a = x as Element of NAT by A3;
a <= n by A3, FINSEQ_1:1;
then a < n + 1 by NAT_1:13;
then A4: a - 1 < (n + 1) - 1 by XREAL_1:14;
consider b being Element of NAT such that
A5: b = a -' 1 ;
1 <= a by A3, FINSEQ_1:1;
then a -' 1 < n by A4, XREAL_1:233;
then [**(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;
hence ex y being object st
( y in Y & S₁[x,y] ) by A5; :: thesis: verum

end;

consider F being Function of (Seg n),Y such that
A6: for x being object st x in Seg n holds
S₁[x,F . x] from FUNCT_2:sch 1(A2);
for c being object 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 object st
( x in Seg n & c = F . x )

proof

let c be object ; :: 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 object st
( x in Seg n & c = F . x ) )
assume c in { [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] where k is Element of NAT : k < n } ; :: thesis: ex x being object st
( x in Seg n & c = F . x )
then consider k being Element of NAT such that
A7: c = [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] and
A8: k < n ;
A9: (k + 1) -' 1 = k by NAT_D:34;
( 0 + 1 <= k + 1 & k + 1 <= n ) by A8, INT_1:7;
then A10: k + 1 in Seg n by FINSEQ_1:1;
then ex j being Element of NAT st
( j = k + 1 & F . (k + 1) = [**(cos (((2 * PI) * (j -' 1)) / n)),(sin (((2 * PI) * (j -' 1)) / n))**] ) by A6;
hence ex x being object st
( x in Seg n & c = F . x ) by A7, A10, A9; :: thesis: verum

end;

then A11: rng F = { [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] where k is Element of NAT : k < n } by FUNCT_2:10;
A12: dom F = Seg n by FUNCT_2:def 1;
for x1, x2 being object st x1 in dom F & x2 in dom F & F . x1 = F . x2 holds
x1 = x2

proof

let x1, x2 be object ; :: thesis: ( x1 in dom F & x2 in dom F & F . x1 = F . x2 implies x1 = x2 )
assume that
A13: x1 in dom F and
A14: x2 in dom F and
A15: F . x1 = F . x2 ; :: thesis: x1 = x2
A16: x1 in Seg n by A13, FUNCT_2:def 1;
then consider j being Element of NAT such that
A17: j = x1 and
A18: F . x1 = [**(cos (((2 * PI) * (j -' 1)) / n)),(sin (((2 * PI) * (j -' 1)) / n))**] by A6;
set a1 = ((2 * PI) * (j -' 1)) / n;
A19: 1 <= j by A16, A17, FINSEQ_1:1;
j <= n by A16, A17, FINSEQ_1:1;
then j - 1 < n by XREAL_1:146, XXREAL_0:2;
then j -' 1 < n by A19, XREAL_1:233;
then (j -' 1) / n < n / n by XREAL_1:74;
then (j -' 1) / n < 1 by XCMPLX_1:60;
then ((j -' 1) / n) * (2 * PI) < 1 * (2 * PI) by COMPTRIG:5, XREAL_1:68;
then A20: ((2 * PI) * (j -' 1)) / n < 2 * PI by XCMPLX_1:74;
A21: x2 in Seg n by A14, FUNCT_2:def 1;
then consider k being Element of NAT such that
A22: k = x2 and
A23: F . x2 = [**(cos (((2 * PI) * (k -' 1)) / n)),(sin (((2 * PI) * (k -' 1)) / n))**] by A6;
set a2 = ((2 * PI) * (k -' 1)) / n;
A24: 1 <= k by A21, A22, FINSEQ_1:1;
k <= n by A21, A22, FINSEQ_1:1;
then k - 1 < n by XREAL_1:146, XXREAL_0:2;
then k -' 1 < n by A24, XREAL_1:233;
then (k -' 1) / n < n / n by XREAL_1:74;
then (k -' 1) / n < 1 by XCMPLX_1:60;
then ((k -' 1) / n) * (2 * PI) < 1 * (2 * PI) by COMPTRIG:5, XREAL_1:68;
then A25: ((2 * PI) * (k -' 1)) / n < 2 * PI by XCMPLX_1:74;
cos (((2 * PI) * (j -' 1)) / n) = cos (((2 * PI) * (k -' 1)) / n) by A15, A18, A23, COMPLEX1:77;
then ((2 * PI) * (j -' 1)) / n = ((2 * PI) * (k -' 1)) / n by A15, A18, A23, A20, A25, COMPLEX2:11, COMPTRIG:5;
then (((2 * PI) * (j -' 1)) / n) * n = (2 * PI) * (k -' 1) by XCMPLX_1:87;
then j -' 1 = k -' 1 by COMPTRIG:5, XCMPLX_1:5, XCMPLX_1:87;
then j = (k -' 1) + 1 by A19, XREAL_1:235;
hence x1 = x2 by A17, A22, A24, XREAL_1:235; :: thesis: verum

end;

then F is one-to-one by FUNCT_1:def 4;
then Seg n,F .: (Seg n) are_equipotent by A12, CARD_1:33;
then Seg n, rng F are_equipotent by A12, RELAT_1:113;
then card (Seg n) = card { [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] where k is Element of NAT : k < n } by A11, CARD_1:5;
hence card (n -roots_of_1) = n by A1, FINSEQ_1:57; :: thesis: verum