let L be non empty well-unital doubleLoopStr ; :: thesis: for p being Polynomial of L st deg p is odd holds

even_part (Leading-Monomial p) = 0_. L

let p be Polynomial of L; :: thesis: ( deg p is odd implies even_part (Leading-Monomial p) = 0_. L )

assume A1: deg p is odd ; :: thesis: even_part (Leading-Monomial p) = 0_. L

set LMp = Leading-Monomial p;

set e = even_part (Leading-Monomial p);

A2: dom (0_. L) = NAT by FUNCT_2:def 1

.= dom (even_part (Leading-Monomial p)) by FUNCT_2:def 1 ;

even_part (Leading-Monomial p) = 0_. L

let p be Polynomial of L; :: thesis: ( deg p is odd implies even_part (Leading-Monomial p) = 0_. L )

assume A1: deg p is odd ; :: thesis: even_part (Leading-Monomial p) = 0_. L

set LMp = Leading-Monomial p;

set e = even_part (Leading-Monomial p);

A2: dom (0_. L) = NAT by FUNCT_2:def 1

.= dom (even_part (Leading-Monomial p)) by FUNCT_2:def 1 ;

now :: thesis: for x being object st x in dom (0_. L) holds

(even_part (Leading-Monomial p)) . x = (0_. L) . x

hence
even_part (Leading-Monomial p) = 0_. L
by A2, FUNCT_1:2; :: thesis: verum(even_part (Leading-Monomial p)) . x = (0_. L) . x

let x be object ; :: thesis: ( x in dom (0_. L) implies (even_part (Leading-Monomial p)) . x = (0_. L) . x )

assume x in dom (0_. L) ; :: thesis: (even_part (Leading-Monomial p)) . x = (0_. L) . x

then reconsider i = x as Element of NAT by FUNCT_2:def 1;

end;assume x in dom (0_. L) ; :: thesis: (even_part (Leading-Monomial p)) . x = (0_. L) . 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 = (0_. L) . x ) or ( len p <> 0 & (even_part (Leading-Monomial p)) . x = (0_. L) . x ) )end;

hence
(even_part (Leading-Monomial p)) . x = (0_. L) . x
; :: thesis: verumper cases
( len p = 0 or len p <> 0 )
;

end;

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

then
p = 0_. L
by POLYNOM4:5;

then Leading-Monomial p = 0_. L by POLYNOM4:13;

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

end;then Leading-Monomial p = 0_. L by POLYNOM4:13;

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

case
len p <> 0
; :: thesis: (even_part (Leading-Monomial p)) . 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;

end;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 = (0_. L) . i ) or ( i is odd & (even_part (Leading-Monomial p)) . i = (0_. L) . i ) )end;

hence
(even_part (Leading-Monomial p)) . x = (0_. L) . x
; :: thesis: verumper cases
( i is even or i is odd )
;

end;

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

hence (even_part (Leading-Monomial p)) . i =
(Leading-Monomial p) . i
by Def1

.= 0. L by A4, A3, A1, POLYNOM4:def 1

.= (0_. L) . i by FUNCOP_1:7 ;

:: thesis: verum

end;.= 0. L by A4, A3, A1, POLYNOM4:def 1

.= (0_. L) . i by FUNCOP_1:7 ;

:: thesis: verum

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

hence (even_part (Leading-Monomial p)) . i =
0. L
by Def1

.= (0_. L) . i by FUNCOP_1:7 ;

:: thesis: verum

end;.= (0_. L) . i by FUNCOP_1:7 ;

:: thesis: verum