theorem BBB: :: FIELD_15:14

for R being Ring
for q being Element of the carrier of (Polynom-Ring R)
for p being Polynomial of R
for n, j being Nat st p = n * q holds
p . j = n * (q . j)