let L be non empty ZeroStr ; :: thesis: for p being Polynomial of L st len (even_part p) <> 0 holds
len (even_part p) is odd
let p be Polynomial of L; :: thesis: ( len (even_part p) <> 0 implies len (even_part p) is odd )
assume A1: len (even_part p) <> 0 ; :: thesis: len (even_part p) is odd
set E = even_part p;
assume len (even_part p) is even ; :: thesis: contradiction
then consider n being Nat such that
A2: 2 * n = len (even_part p) by ABIAN:def 2;
A3: len (even_part p) is_at_least_length_of even_part p by ALGSEQ_1:def 3;
n <> 0 by A1, A2;
then reconsider n1 = n - 1 as Nat ;
n + n1 is_at_least_length_of even_part p
proof
let k be Nat; :: according to ALGSEQ_1:def 2 :: thesis: ( not n + n1 <= k or (even_part p) . k = 0. L )
assume A4: k >= n + n1 ; :: thesis: (even_part p) . k = 0. L
assume A5: (even_part p) . k <> 0. L ; :: thesis: contradiction
then ( k is even & n + n1 = (2 * n) - 1 ) by HURWITZ2:def 1;
then k > n + n1 by A4, XXREAL_0:1;
then k >= (n + n1) + 1 by NAT_1:13;
hence contradiction by A5, A2, A3, ALGSEQ_1:def 2; :: thesis: verum
end;
then n + n <= n + n1 by ALGSEQ_1:def 3, A2;
then n1 + 1 <= n1 by XREAL_1:8;
hence contradiction by NAT_1:13; :: thesis: verum