set g = Polynomial-Function (L,(p + q));

now :: thesis: for x being Element of L holds (Polynomial-Function (L,(p + q))) . (- x) = - ((Polynomial-Function (L,(p + q))) . x)

let x be Element of L; :: thesis: (Polynomial-Function (L,(p + q))) . (- x) = - ((Polynomial-Function (L,(p + q))) . x)
thus (Polynomial-Function (L,(p + q))) . (- x) = eval ((p + q),(- x)) by POLYNOM5:def 13
.= (eval (p,(- x))) + (eval (q,(- x))) by POLYNOM4:19
.= (- (eval (p,x))) + (eval (q,(- x))) by Th25
.= (- (eval (p,x))) + (- (eval (q,x))) by Th25
.= - ((eval (p,x)) + (eval (q,x))) by RLVECT_1:31
.= - (eval ((p + q),x)) by POLYNOM4:19
.= - ((Polynomial-Function (L,(p + q))) . x) by POLYNOM5:def 13 ; :: thesis: verum

end;

then Polynomial-Function (L,(p + q)) is odd ;
hence p + q is odd ; :: thesis: verum