let n be Nat; len (sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)),2)) = n + 1
set PPn = <%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1);
A1:
n + 1 is_at_least_length_of sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)),2)
for m being Nat st m is_at_least_length_of sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)),2) holds
n + 1 <= m
hence
len (sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)),2)) = n + 1
by A1, ALGSEQ_1:def 3; verum