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))

proof

let k be Nat; :: according to ALGSEQ_1:def 2 :: thesis: ( not 0 <= k or (sieve (p,(2 * n))) . k = 0. L )
assume k >= 0 ; :: thesis: (sieve (p,(2 * n))) . k = 0. L
thus (sieve (p,(2 * n))) . k = p . ((2 * n) * k) by Def5
.= (even_part p) . ((2 * n) * k) by HURWITZ2:def 1
.= 0. L by A2, ALGSEQ_1:def 2 ; :: thesis: verum

end;

hence len (sieve (p,(2 * n))) = 0 by ALGSEQ_1:def 3; :: thesis: verum