let L be non empty well-unital doubleLoopStr ; :: thesis: for p being even Polynomial of L

for x being Element of L holds eval (p,(- x)) = eval (p,x)

let p be even Polynomial of L; :: thesis: for x being Element of L holds eval (p,(- x)) = eval (p,x)

let x be Element of L; :: thesis: eval (p,(- x)) = eval (p,x)

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

.= (Polynomial-Function (L,p)) . x by Def3, Def5

.= eval (p,x) by POLYNOM5:def 13 ; :: thesis: verum

for x being Element of L holds eval (p,(- x)) = eval (p,x)

let p be even Polynomial of L; :: thesis: for x being Element of L holds eval (p,(- x)) = eval (p,x)

let x be Element of L; :: thesis: eval (p,(- x)) = eval (p,x)

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

.= (Polynomial-Function (L,p)) . x by Def3, Def5

.= eval (p,x) by POLYNOM5:def 13 ; :: thesis: verum