theorem Th69: :: NUMBER19:69

for L being non empty non degenerated right_complementable Abelian add-associative right_zeroed well-unital distributive unital associative commutative domRing-like doubleLoopStr
for p being Polynomial of L st p . 0 <> 0. L holds
ex q being Polynomial of L st
( len p = len q & q . 0 = 1. L & ( for i being Element of NAT st 0 < i holds
q . i = (p . i) * ((power L) . ((p . 0),(i -' 1))) ) & ( for x being Element of L holds eval (p,((p . 0) * x)) = (p . 0) * (eval (q,x)) ) )