let L be non degenerated right_complementable Abelian add-associative right_zeroed well-unital doubleLoopStr ; 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; for x being Element of L holds eval (p,(- x)) = - (eval (p,x))
let x be Element of L; 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
; verum