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

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