theorem Th22: :: POLYNOM5:22

for L being non empty non degenerated right_complementable Abelian add-associative right_zeroed well-unital distributive associative commutative doubleLoopStr
for p being Polynomial of L
for x being Element of L
for n being Nat holds eval ((p `^ n),x) = (power L) . ((eval (p,x)),n)