theorem prl0a: :: RING_5:5

for R being domRing
for p being Polynomial of R
for a being Element of R holds LC (a * p) = a * (LC p)