let L be non empty well-unital doubleLoopStr ; :: thesis: for p being Polynomial of L st deg p is even holds
even_part (Leading-Monomial p) = Leading-Monomial p
let p be Polynomial of L; :: thesis: ( deg p is even implies even_part (Leading-Monomial p) = Leading-Monomial p )
assume A1: deg p is even ; :: thesis: even_part (Leading-Monomial p) = Leading-Monomial p
set LMp = Leading-Monomial p;
set e = even_part (Leading-Monomial p);
A2: dom (even_part (Leading-Monomial p)) = NAT by FUNCT_2:def 1
.= dom (Leading-Monomial p) by FUNCT_2:def 1 ;

now :: thesis: for x being object st x in dom (even_part (Leading-Monomial p)) holds
(even_part (Leading-Monomial p)) . x = (Leading-Monomial p) . x

let x be object ; :: thesis: ( x in dom (even_part (Leading-Monomial p)) implies (even_part (Leading-Monomial p)) . x = (Leading-Monomial p) . x )
assume x in dom (even_part (Leading-Monomial p)) ; :: thesis: (even_part (Leading-Monomial p)) . x = (Leading-Monomial p) . x
then reconsider i = x as Element of NAT by FUNCT_2:def 1;

now :: thesis: ( ( len p = 0 & (even_part (Leading-Monomial p)) . x = (Leading-Monomial p) . x ) or ( len p <> 0 & (even_part (Leading-Monomial p)) . x = (Leading-Monomial p) . x ) )

per cases ( len p = 0 or len p <> 0 ) ;

case len p = 0 ; :: thesis: (even_part (Leading-Monomial p)) . x = (Leading-Monomial p) . x

then p = 0_. L by POLYNOM4:5;
then Leading-Monomial p = 0_. L by POLYNOM4:13;
hence (even_part (Leading-Monomial p)) . x = (Leading-Monomial p) . x by Th7; :: thesis: verum

end;

case len p <> 0 ; :: thesis: (even_part (Leading-Monomial p)) . x = (Leading-Monomial p) . x

then (len p) + 1 > 0 + 1 by XREAL_1:8;
then len p >= 1 by NAT_1:13;
then A3: (len p) -' 1 = deg p by XREAL_1:233;

now :: thesis: ( ( i is even & (even_part (Leading-Monomial p)) . i = (Leading-Monomial p) . i ) or ( i is odd & (Leading-Monomial p) . i = (even_part (Leading-Monomial p)) . i ) )

per cases ( i is even or i is odd ) ;

case i is even ; :: thesis: (even_part (Leading-Monomial p)) . i = (Leading-Monomial p) . i

hence (even_part (Leading-Monomial p)) . i = (Leading-Monomial p) . i by Def1; :: thesis: verum

end;

case A4: i is odd ; :: thesis: (Leading-Monomial p) . i = (even_part (Leading-Monomial p)) . i

hence (Leading-Monomial p) . i = 0. L by A3, A1, POLYNOM4:def 1
.= (even_part (Leading-Monomial p)) . i by A4, Def1 ;
:: thesis: verum

end;

end;

end;

hence (even_part (Leading-Monomial p)) . x = (Leading-Monomial p) . x ; :: thesis: verum

end;

end;

end;

hence (even_part (Leading-Monomial p)) . x = (Leading-Monomial p) . x ; :: thesis: verum

end;

hence even_part (Leading-Monomial p) = Leading-Monomial p by A2, FUNCT_1:2; :: thesis: verum