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

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

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

end;

then Polynomial-Function (L,(1_. L)) is even ;
hence 1_. L is even ; :: thesis: verum