let L be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for p being Polynomial of L holds p - (even_part p) = odd_part p
let p be Polynomial of L; :: thesis: p - (even_part p) = odd_part p
set e = even_part p;
set o = odd_part p;
A1: dom (p - (even_part p)) = NAT by FUNCT_2:def 1
.= dom (odd_part p) by FUNCT_2:def 1 ;

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

let x be object ; :: thesis: ( x in dom (odd_part p) implies (p - (even_part p)) . x = (odd_part p) . x )
assume x in dom (odd_part p) ; :: thesis: (p - (even_part p)) . x = (odd_part p) . x
then reconsider i = x as Element of NAT by FUNCT_2:def 1;
p = (odd_part p) + (even_part p) by Th10;
then p . i = ((odd_part p) . i) + ((even_part p) . i) by NORMSP_1:def 2;
then (p . i) - ((even_part p) . i) = ((odd_part p) . i) + (((even_part p) . i) + (- ((even_part p) . i))) by RLVECT_1:def 3
.= ((odd_part p) . i) + (0. L) by RLVECT_1:5
.= (odd_part p) . i by RLVECT_1:def 4 ;
hence (p - (even_part p)) . x = (odd_part p) . x by POLYNOM3:27; :: thesis: verum

end;

hence p - (even_part p) = odd_part p by A1, FUNCT_1:2; :: thesis: verum