theorem Th30: :: POLYNOM9:30

for k being Nat
for O being Ordinal
for R being non trivial right_complementable associative commutative Abelian add-associative right_zeroed right_unital well-unital distributive doubleLoopStr
for p being Polynomial of O,R
for f being Function of O,R holds eval ((p `^ k),f) = (power R) . ((eval (p,f)),k)