set f = Polynomial-Function (L,(0_. L));

now :: thesis: for x being Element of L holds (Polynomial-Function (L,(0_. L))) . (- x) = - ((Polynomial-Function (L,(0_. L))) . x)

let x be Element of L; :: thesis: (Polynomial-Function (L,(0_. L))) . (- x) = - ((Polynomial-Function (L,(0_. L))) . x)
thus (Polynomial-Function (L,(0_. L))) . (- x) = eval ((0_. L),(- x)) by POLYNOM5:def 13
.= 0. L by POLYNOM4:17
.= - (0. L) by RLVECT_1:12
.= - (eval ((0_. L),x)) by POLYNOM4:17
.= - ((Polynomial-Function (L,(0_. L))) . x) by POLYNOM5:def 13 ; :: thesis: verum

end;

hence 0_. L is odd by Def4; :: thesis: verum