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