theorem :: FIELD_15:32

for R being non degenerated comRing
for a, b being Element of R
for n being Nat holds eval (((X+ a) `^ n),b) = (a + b) |^ n