set p = 0_. L;

take 0_. L ; :: thesis: 0_. L is even

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

take 0_. L ; :: thesis: 0_. L is even

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

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

let x be Element of L; :: thesis: (Polynomial-Function (L,(0_. L))) . x = 0. L

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

.= 0. L by POLYNOM4:17 ; :: thesis: verum

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

.= 0. L by POLYNOM4:17 ; :: thesis: verum

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

hence
0_. L is even
by Def3; :: thesis: verumlet 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) = 0. L by A1

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

end;thus (Polynomial-Function (L,(0_. L))) . (- x) = 0. L by A1

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