let n be non zero Element of NAT ; :: thesis: card () = n
set X = { [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] where k is Element of NAT : k < n } ;
defpred S1[ 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 & S1[x,y] )
proof
let x be object ; :: thesis: ( x in Seg n implies ex y being object st
( y in Y & S1[x,y] ) )

assume A3: x in Seg n ; :: thesis: ex y being object st
( y in Y & S1[x,y] )

reconsider a = x as Element of NAT by A3;
a <= n by ;
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 ;
then a -' 1 < n by ;
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 & S1[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
S1[x,F . x] from 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 ;
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 ;
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 ;
j <= n by ;
then j - 1 < n by ;
then j -' 1 < n by ;
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 ;
then A20: ((2 * PI) * (j -' 1)) / n < 2 * PI by XCMPLX_1:74;
A21: x2 in Seg n by ;
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 ;
k <= n by ;
then k - 1 < n by ;
then k -' 1 < n by ;
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 ;
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 ;
then ((2 * PI) * (j -' 1)) / n = ((2 * PI) * (k -' 1)) / n by ;
then (((2 * PI) * (j -' 1)) / n) * n = (2 * PI) * (k -' 1) by XCMPLX_1:87;
then j -' 1 = k -' 1 by ;
then j = (k -' 1) + 1 by ;
hence x1 = x2 by ; :: thesis: verum
end;
then F is one-to-one by FUNCT_1:def 4;
then Seg n,F .: (Seg n) are_equipotent by ;
then Seg n, rng F are_equipotent by ;
then card (Seg n) = card { [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] where k is Element of NAT : k < n } by ;
hence card () = n by ; :: thesis: verum