let L be non empty well-unital doubleLoopStr ; :: thesis: for p being Polynomial of L st deg p is odd holds
even_part () = 0_. L

let p be Polynomial of L; :: thesis: ( deg p is odd implies even_part () = 0_. L )
assume A1: deg p is odd ; :: thesis:
set LMp = Leading-Monomial p;
set e = even_part ();
A2: dom (0_. L) = NAT by FUNCT_2:def 1
.= dom () by FUNCT_2:def 1 ;
now :: thesis: for x being object st x in dom (0_. L) holds
() . x = (0_. L) . x
let x be object ; :: thesis: ( x in dom (0_. L) implies () . x = (0_. L) . x )
assume x in dom (0_. L) ; :: thesis: () . x = (0_. L) . x
then reconsider i = x as Element of NAT by FUNCT_2:def 1;
now :: thesis: ( ( len p = 0 & () . x = (0_. L) . x ) or ( len p <> 0 & () . x = (0_. L) . x ) )
per cases ( len p = 0 or len p <> 0 ) ;
case len p <> 0 ; :: thesis: () . x = (0_. L) . 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 & () . i = (0_. L) . i ) or ( i is odd & () . i = (0_. L) . i ) )
per cases ( i is even or i is odd ) ;
case A4: i is even ; :: thesis: () . i = (0_. L) . i
hence () . i = () . i by Def1
.= 0. L by
.= (0_. L) . i by FUNCOP_1:7 ;
:: thesis: verum
end;
case i is odd ; :: thesis: () . i = (0_. L) . i
hence () . i = 0. L by Def1
.= (0_. L) . i by FUNCOP_1:7 ;
:: thesis: verum
end;
end;
end;
hence (even_part ()) . x = (0_. L) . x ; :: thesis: verum
end;
end;
end;
hence (even_part ()) . x = (0_. L) . x ; :: thesis: verum
end;
hence even_part () = 0_. L by ; :: thesis: verum