theorem lcrpol: :: RING_5:9

for R being non degenerated Ring
for a being Element of R
for k being non zero Element of NAT holds LC (rpoly (k,a)) = 1. R