theorem thE2: :: FIELD_6:7

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