theorem Th27: :: RINGDER1:27

for R being domRing
for a being Element of R
for i being Nat
for p being Element of the carrier of (Polynom-Ring R) holds ((a | R) *' p) . i = a * (p . i)