set p = 1_. L;
take 1_. L ; :: thesis: ( not 1_. L is zero & 1_. L is even )
set f = Polynomial-Function (L,(1_. L));

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

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

end;

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) = 1. L by A1
.= (Polynomial-Function (L,(1_. L))) . x by A1 ; :: thesis: verum

end;

hence ( not 1_. L is zero & 1_. L is even ) by Def3; :: thesis: verum