defpred S₁[ Nat] means for p being Polynomial of L st len p = L holds
even_part p is even ;

A1: now :: thesis: for k being Nat st ( for n being Nat st n < k holds
S₁[n] ) holds
S₁[k]

let k be Nat; :: thesis: ( ( for n being Nat st n < k holds
S₁[n] ) implies S₁[k] )
assume A2: for n being Nat st n < k holds
S₁[n] ; :: thesis: S₁[k]

now :: thesis: for p being Polynomial of L st len p = k holds
even_part p is even

let p be Polynomial of L; :: thesis: ( len p = k implies even_part p is even )
assume A3: len p = k ; :: thesis: even_part p is even

now :: thesis: ( ( k = 0 & even_part p is even ) or ( k <> 0 & even_part p is even ) )

per cases ( k = 0 or k <> 0 ) ;

case k = 0 ; :: thesis: even_part p is even

then p = 0_. L by A3, POLYNOM4:5;
hence even_part p is even by Th7; :: thesis: verum

end;

case A4: k <> 0 ; :: thesis: even_part p is even

set LMp = Leading-Monomial p;
set g = Polynomial-Function (L,(Leading-Monomial p));
(Leading-Monomial p) + (p - (Leading-Monomial p)) = ((Leading-Monomial p) + (- (Leading-Monomial p))) + p by POLYNOM3:26
.= ((Leading-Monomial p) - (Leading-Monomial p)) + p
.= (0_. L) + p by POLYNOM3:29
.= p by POLYNOM3:28 ;
then A5: even_part p = (even_part (Leading-Monomial p)) + (even_part (p - (Leading-Monomial p))) by Th15;
consider t being Polynomial of L such that
A6: ( len t < len p & p = t + (Leading-Monomial p) & ( for n being Element of NAT st n < (len p) - 1 holds
t . n = p . n ) ) by A4, A3, POLYNOM4:16;
p - (Leading-Monomial p) = t + ((Leading-Monomial p) - (Leading-Monomial p)) by A6, POLYNOM3:26
.= t + (0_. L) by POLYNOM3:29
.= t by POLYNOM3:28 ;
then A7: even_part (p - (Leading-Monomial p)) is even by A6, A2, A3;

now :: thesis: ( ( deg p is even & even_part (Leading-Monomial p) is even ) or ( deg p is odd & even_part (Leading-Monomial p) is even ) )

per cases ( deg p is even or deg p is odd ) ;

case A8: deg p is even ; :: thesis: even_part (Leading-Monomial p) is even

now :: thesis: for x being Element of L holds (Polynomial-Function (L,(Leading-Monomial p))) . x = (Polynomial-Function (L,(Leading-Monomial p))) . (- x)

let x be Element of L; :: thesis: (Polynomial-Function (L,(Leading-Monomial p))) . x = (Polynomial-Function (L,(Leading-Monomial p))) . (- x)
(len p) + 1 > 0 + 1 by A3, A4, XREAL_1:8;
then len p >= 1 by NAT_1:13;
then A9: (len p) -' 1 = deg p by XREAL_1:233;
thus (Polynomial-Function (L,(Leading-Monomial p))) . x = eval ((Leading-Monomial p),x) by POLYNOM5:def 13
.= (p . ((len p) -' 1)) * ((power L) . (x,((len p) -' 1))) by POLYNOM4:22
.= (p . ((len p) -' 1)) * ((power L) . ((- x),((len p) -' 1))) by A9, A8, Th3
.= eval ((Leading-Monomial p),(- x)) by POLYNOM4:22
.= (Polynomial-Function (L,(Leading-Monomial p))) . (- x) by POLYNOM5:def 13 ; :: thesis: verum

end;

then Polynomial-Function (L,(Leading-Monomial p)) is even ;
hence even_part (Leading-Monomial p) is even by A8, Th17; :: thesis: verum

end;

case deg p is odd ; :: thesis: even_part (Leading-Monomial p) is even

then even_part (Leading-Monomial p) = 0_. L by Th18;
hence even_part (Leading-Monomial p) is even ; :: thesis: verum

end;

end;

end;

hence even_part p is even by A7, A5; :: thesis: verum

end;

end;

end;

hence even_part p is even ; :: thesis: verum

end;

hence S₁[k] ; :: thesis: verum

end;

A10: for k being Nat holds S₁[k] from NAT_1:sch 4(A1);
consider k being Nat such that
A11: len p = k ;
thus even_part p is even by A11, A10; :: thesis: verum