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

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

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

end;

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