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

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

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

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

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

case A2: i is even ; :: thesis: ((odd_part p) /. i) + ((even_part p) /. i) = p /. i

hence ((odd_part p) /. i) + ((even_part p) /. i) = (0. L) + ((even_part p) . i) by Def2
.= (even_part p) . i by ALGSTR_1:def 2
.= p /. i by Def1, A2 ;
:: thesis: verum

end;

case A3: i is odd ; :: thesis: ((odd_part p) /. i) + ((even_part p) /. i) = p /. i

hence ((odd_part p) /. i) + ((even_part p) /. i) = ((odd_part p) . i) + (0. L) by Def1
.= (odd_part p) . i by RLVECT_1:def 4
.= p /. i by Def2, A3 ;
:: thesis: verum

end;

end;

end;

hence p . x = ((odd_part p) + (even_part p)) . x by NORMSP_1:def 2; :: thesis: verum

end;

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