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

then n1 + 1 <= n1 by XREAL_1:8;

hence contradiction by NAT_1:13; :: thesis: verum

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

then
n + n <= n + n1
by ALGSEQ_1:def 3, A2;
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;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

then n1 + 1 <= n1 by XREAL_1:8;

hence contradiction by NAT_1:13; :: thesis: verum