theorem thE1: :: FIELD_6:6

for R being Ring
for p being Polynomial of R
for i being Nat holds (<%(0. R),(1. R)%> *' p) . (i + 1) = p . i