let L be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; :: thesis: for p, q being Polynomial of L holds odd_part (p + q) = (odd_part p) + (odd_part q)
let p, q be Polynomial of L; :: thesis: odd_part (p + q) = (odd_part p) + (odd_part q)
set opq = odd_part (p + q);
set op = odd_part p;
set oq = odd_part q;
A1: dom (odd_part (p + q)) = NAT by FUNCT_2:def 1
.= dom ((odd_part p) + (odd_part q)) by FUNCT_2:def 1 ;

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

let x be object ; :: thesis: ( x in dom (odd_part (p + q)) implies ((odd_part p) + (odd_part q)) . x = (odd_part (p + q)) . x )
assume x in dom (odd_part (p + q)) ; :: thesis: ((odd_part p) + (odd_part q)) . x = (odd_part (p + q)) . x
then reconsider i = x as Element of NAT by FUNCT_2:def 1;

now :: thesis: ( ( i is odd & ((odd_part p) + (odd_part q)) . i = (odd_part (p + q)) . i ) or ( i is even & ((odd_part p) + (odd_part q)) . i = (odd_part (p + q)) . i ) )

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

case A2: i is odd ; :: thesis: ((odd_part p) + (odd_part q)) . i = (odd_part (p + q)) . i

thus ((odd_part p) + (odd_part q)) . i = ((odd_part p) . i) + ((odd_part q) . i) by NORMSP_1:def 2
.= (p . i) + ((odd_part q) . i) by A2, Def2
.= (p . i) + (q . i) by A2, Def2
.= (p + q) . i by NORMSP_1:def 2
.= (odd_part (p + q)) . i by A2, Def2 ; :: thesis: verum

end;

case A3: i is even ; :: thesis: ((odd_part p) + (odd_part q)) . i = (odd_part (p + q)) . i

thus ((odd_part p) + (odd_part q)) . i = ((odd_part p) . i) + ((odd_part q) . i) by NORMSP_1:def 2
.= (0. L) + ((odd_part q) . i) by A3, Def2
.= (0. L) + (0. L) by A3, Def2
.= 0. L by RLVECT_1:def 4
.= (odd_part (p + q)) . i by A3, Def2 ; :: thesis: verum

end;

end;

end;

hence ((odd_part p) + (odd_part q)) . x = (odd_part (p + q)) . x ; :: thesis: verum

end;

hence odd_part (p + q) = (odd_part p) + (odd_part q) by A1, FUNCT_1:2; :: thesis: verum