theorem Th22: :: POLYNOM4:22

for L being non empty right_complementable add-associative right_zeroed distributive unital doubleLoopStr
for p being Polynomial of L
for x being Element of L holds eval ((Leading-Monomial p),x) = (p . ((len p) -' 1)) * ((power L) . (x,((len p) -' 1)))