let L be non degenerated right_complementable Abelian add-associative right_zeroed well-unital doubleLoopStr ; :: thesis: for p being odd Polynomial of L
for x being Element of L holds eval (p,(- x)) = - (eval (p,x))
let p be odd 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))
A1: Polynomial-Function (L,p) is odd by Def6;
thus eval (p,(- x)) = (Polynomial-Function (L,p)) . (- x) by POLYNOM5:def 13
.= - ((Polynomial-Function (L,p)) . x) by A1
.= - (eval (p,x)) by POLYNOM5:def 13 ; :: thesis: verum