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