set p = 1_. L;

take 1_. L ; :: thesis: ( not 1_. L is zero & 1_. L is even )

set f = Polynomial-Function (L,(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;thus (Polynomial-Function (L,(1_. L))) . x = eval ((1_. L),x) by POLYNOM5:def 13

.= 1. L by POLYNOM4:18 ; :: thesis: verum

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

hence
( not 1_. L is zero & 1_. L is even )
by Def3; :: thesis: verumlet 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;thus (Polynomial-Function (L,(1_. L))) . (- x) = 1. L by A1

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