let L be non empty ZeroStr ; :: thesis: for p being Polynomial of L st len (even_part p) = 0 holds
for n being non zero Nat holds len (sieve (p,(2 * n))) = 0
let p be Polynomial of L; :: thesis: ( len (even_part p) = 0 implies for n being non zero Nat holds len (sieve (p,(2 * n))) = 0 )
assume A1: len (even_part p) = 0 ; :: thesis: for n being non zero Nat holds len (sieve (p,(2 * n))) = 0
let n be non zero Nat; :: thesis: len (sieve (p,(2 * n))) = 0
A2: 0 is_at_least_length_of even_part p by A1, ALGSEQ_1:def 3;
0 is_at_least_length_of sieve (p,(2 * n)) hence len (sieve (p,(2 * n))) = 0 by ALGSEQ_1:def 3; :: thesis: verum