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

hence 0_. L is even ; :: thesis: verum

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

then
Polynomial-Function (L,(0_. L)) is even
;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

.= eval ((0_. L),x) by POLYNOM4:17

.= (Polynomial-Function (L,(0_. L))) . x by POLYNOM5:def 13 ; :: thesis: verum

end;thus (Polynomial-Function (L,(0_. L))) . (- x) = eval ((0_. L),(- x)) by POLYNOM5:def 13

.= 0. L by POLYNOM4:17

.= eval ((0_. L),x) by POLYNOM4:17

.= (Polynomial-Function (L,(0_. L))) . x by POLYNOM5:def 13 ; :: thesis: verum

hence 0_. L is even ; :: thesis: verum