let L be non empty ZeroStr ; :: thesis: for p being Polynomial of L st len (even_part p) is odd holds
2 * (len (sieve (p,2))) = (len (even_part p)) + 1
let p be Polynomial of L; :: thesis: ( len (even_part p) is odd implies 2 * (len (sieve (p,2))) = (len (even_part p)) + 1 )
set E = even_part p;
set CE = sieve ((even_part p),2);
assume len (even_part p) is odd ; :: thesis: 2 * (len (sieve (p,2))) = (len (even_part p)) + 1
then consider n being Nat such that
A1: len (even_part p) = (2 * n) + 1 by ABIAN:9;
A2: len (even_part p) is_at_least_length_of even_part p by ALGSEQ_1:def 3;
set n1 = n + 1;
A3: n + 1 is_at_least_length_of sieve ((even_part p),2)

proof

let k be Nat; :: according to ALGSEQ_1:def 2 :: thesis: ( not n + 1 <= k or (sieve ((even_part p),2)) . k = 0. L )
assume A4: k >= n + 1 ; :: thesis: (sieve ((even_part p),2)) . k = 0. L
( k + k >= (n + 1) + (n + 1) & (n + 1) + (n + 1) = (len (even_part p)) + 1 ) by A1, A4, XREAL_1:7;
then k + k > len (even_part p) by NAT_1:13;
hence 0. L = (even_part p) . (2 * k) by A2, ALGSEQ_1:def 2
.= (sieve ((even_part p),2)) . k by Def5 ;
:: thesis: verum

end;

for m being Nat st m is_at_least_length_of sieve ((even_part p),2) holds
n + 1 <= m

proof

let m be Nat; :: thesis: ( m is_at_least_length_of sieve ((even_part p),2) implies n + 1 <= m )
assume A5: m is_at_least_length_of sieve ((even_part p),2) ; :: thesis: n + 1 <= m
m > 0

proof

assume A6: m <= 0 ; :: thesis: contradiction
2 * n is_at_least_length_of even_part p

proof

let k be Nat; :: according to ALGSEQ_1:def 2 :: thesis: ( not 2 * n <= k or (even_part p) . k = 0. L )
assume A7: k >= 2 * n ; :: thesis: (even_part p) . k = 0. L

per cases ( k > 2 * n or k = 2 * n ) by A7, XXREAL_0:1;

suppose k > 2 * n ; :: thesis: (even_part p) . k = 0. L

then k >= (2 * n) + 1 by NAT_1:13;
hence (even_part p) . k = 0. L by A1, A2, ALGSEQ_1:def 2; :: thesis: verum

end;

suppose k = 2 * n ; :: thesis: (even_part p) . k = 0. L

hence (even_part p) . k = (sieve ((even_part p),2)) . n by Def5
.= 0. L by A5, A6, ALGSEQ_1:def 2 ;
:: thesis: verum

end;

end;

end;

then (2 * n) + 1 <= 2 * n by A1, ALGSEQ_1:def 3;
hence contradiction by NAT_1:13; :: thesis: verum

end;

then reconsider mm = m - 1 as Nat ;
m + mm is_at_least_length_of even_part p

proof

let k be Nat; :: according to ALGSEQ_1:def 2 :: thesis: ( not m + mm <= k or (even_part p) . k = 0. L )
assume A8: k >= m + mm ; :: thesis: (even_part p) . k = 0. L
assume A9: (even_part p) . k <> 0. L ; :: thesis: contradiction
then A10: k is even by HURWITZ2:def 1;
then consider i being Nat such that
A11: k = 2 * i by ABIAN:def 2;
m + mm = (2 * m) - 1 ;
then k > m + mm by A10, A8, XXREAL_0:1;
then k >= (m + mm) + 1 by NAT_1:13;
then 2 * i >= 2 * m by A11;
then i >= m by XREAL_1:68;
then (sieve ((even_part p),2)) . i = 0. L by A5, ALGSEQ_1:def 2;
hence contradiction by A9, Def5, A11; :: thesis: verum

end;

then len (even_part p) <= m + mm by ALGSEQ_1:def 3;
then ((2 * n) + 1) + 1 <= ((2 * m) - 1) + 1 by A1, XREAL_1:7;
then 2 * (n + 1) <= 2 * m ;
hence n + 1 <= m by XREAL_1:68; :: thesis: verum

end;

then A12: len (sieve ((even_part p),2)) = n + 1 by A3, ALGSEQ_1:def 3;
sieve ((even_part p),2) = sieve (p,(2 * 1)) by Th19;
hence 2 * (len (sieve (p,2))) = (len (even_part p)) + 1 by A1, A12; :: thesis: verum