theorem evalq: :: FIELD_9:20

for R being Ring
for a, b, c, x being Element of R holds eval (<%c,b,a%>,x) = (c + (b * x)) + (a * (x ^2))