let n be Nat; Roots (sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)),2)) = rng (sqr (cot (x_r-seq n)))
set f = x_r-seq n;
set F = sqr (cot (x_r-seq n));
set C = sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)),2);
A1:
( len (sqr (cot (x_r-seq n))) = len (cot (x_r-seq n)) & len (cot (x_r-seq n)) = len (x_r-seq n) & len (x_r-seq n) = n )
by CARD_1:def 7, BASEL_1:21;
sqr (cot (x_r-seq n)) is one-to-one
by BASEL_1:28;
then A2:
( card (dom (sqr (cot (x_r-seq n)))) = card (rng (sqr (cot (x_r-seq n)))) & dom (sqr (cot (x_r-seq n))) = Seg n )
by A1, CARD_1:70, FINSEQ_1:def 3;
A3:
rng (sqr (cot (x_r-seq n))) c= Roots (sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)),2))
by Th26;
A4:
n <= card (Roots (sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)),2)))
by A2, NAT_1:43, Th26;
card (Roots (sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)),2))) < len (sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)),2))
by Th11;
then
card (Roots (sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)),2))) < n + 1
by Th25;
then
card (Roots (sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)),2))) <= n
by NAT_1:13;
hence
Roots (sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)),2)) = rng (sqr (cot (x_r-seq n)))
by A3, CARD_2:102, A2, A4, XXREAL_0:1; verum