defpred S1[ Nat] means for p being Polynomial of L st len p = L holds
odd_part p is odd ;
A12: now :: thesis: for k being Nat st ( for n being Nat st n < k holds
S1[n] ) holds
S1[k]
let k be Nat; :: thesis: ( ( for n being Nat st n < k holds
S1[n] ) implies S1[k] )

assume A13: for n being Nat st n < k holds
S1[n] ; :: thesis: S1[k]
now :: thesis: for p being Polynomial of L st len p = k holds
odd_part p is odd
let p be Polynomial of L; :: thesis: ( len p = k implies odd_part p is odd )
assume A14: len p = k ; :: thesis: odd_part p is odd
now :: thesis: ( ( k = 0 & odd_part p is odd ) or ( k <> 0 & odd_part p is odd ) )
per cases ( k = 0 or k <> 0 ) ;
case A15: k <> 0 ; :: thesis: odd_part p is odd
set LMp = Leading-Monomial p;
set g = Polynomial-Function (L,());
() + (p - ()) = (() + ()) + p by POLYNOM3:26
.= () + p
.= (0_. L) + p by POLYNOM3:29
.= p by POLYNOM3:28 ;
then A16: odd_part p = () + (odd_part (p - ())) by Th16;
consider t being Polynomial of L such that
A17: ( len t < len p & p = t + () & ( for n being Element of NAT st n < (len p) - 1 holds
t . n = p . n ) ) by ;
p - () = t + () by
.= t + (0_. L) by POLYNOM3:29
.= t by POLYNOM3:28 ;
then A18: odd_part (p - ()) is odd by ;
now :: thesis: ( ( deg p is odd & odd_part () is odd ) or ( deg p is even & odd_part () is odd ) )
per cases ( deg p is odd or deg p is even ) ;
case A19: deg p is odd ; :: thesis:
then A20: odd_part () = Leading-Monomial p by Th20;
now :: thesis: for x being Element of L holds - (() . x) = () . (- x)
let x be Element of L; :: thesis: - (() . x) = () . (- x)
(len p) + 1 > 0 + 1 by ;
then len p >= 1 by NAT_1:13;
then A21: (len p) -' 1 = deg p by XREAL_1:233;
thus - (() . x) = - (eval ((),x)) by POLYNOM5:def 13
.= - ((p . ((len p) -' 1)) * (() . (x,((len p) -' 1)))) by POLYNOM4:22
.= (p . ((len p) -' 1)) * (- (() . (x,((len p) -' 1)))) by VECTSP_1:8
.= (p . ((len p) -' 1)) * (() . ((- x),((len p) -' 1))) by
.= eval ((),(- x)) by POLYNOM4:22
.= () . (- x) by POLYNOM5:def 13 ; :: thesis: verum
end;
hence odd_part () is odd by ; :: thesis: verum
end;
end;
end;
hence odd_part p is odd by ; :: thesis: verum
end;
end;
end;
hence odd_part p is odd ; :: thesis: verum
end;
hence S1[k] ; :: thesis: verum
end;
A22: for k being Nat holds S1[k] from consider k being Nat such that
A23: len p = k ;
thus odd_part p is odd by ; :: thesis: verum