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

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

hence
len (sieve (p,(2 * n))) = 0
by ALGSEQ_1:def 3; :: thesis: verum
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;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