let R be domRing; :: thesis: for p being Polynomial of R

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

let p be Polynomial of R; :: thesis: for a being Element of R holds LC (a * p) = a * (LC p)

let a be Element of R; :: thesis: LC (a * p) = a * (LC p)

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

let p be Polynomial of R; :: thesis: for a being Element of R holds LC (a * p) = a * (LC p)

let a be Element of R; :: thesis: LC (a * p) = a * (LC p)