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 Th24
.= (eval (p,x)) + (eval (q,x)) by Th24
.= eval ((p + q),x) by POLYNOM4:19
.= (Polynomial-Function (L,(p + q))) . x by POLYNOM5:def 13 ; :: thesis: verum

end;

hence p + q is even by Def3; :: thesis: verum