let F be Field; :: thesis: for p being Ppoly of F
for a being Element of F holds LC (a * p) = a
let q be Ppoly of F; :: thesis: for a being Element of F holds LC (a * q) = a
let a be Element of F; :: thesis: LC (a * q) = a
thus LC (a * q) = a * (LC q) by RING_5:5
.= a * (1. F) by RING_5:50
.= a ; :: thesis: verum