let R be non degenerated Ring; :: thesis: for a being Element of R
for k being non zero Element of NAT holds LC (rpoly (k,a)) = 1. R
let a be Element of R; :: thesis: for k being non zero Element of NAT holds LC (rpoly (k,a)) = 1. R
let k be non zero Element of NAT ; :: thesis: LC (rpoly (k,a)) = 1. R
deg (rpoly (k,a)) = (len (rpoly (k,a))) - 1 by HURWITZ:def 2;
then k = (len (rpoly (k,a))) - 1 by HURWITZ:27;
hence LC (rpoly (k,a)) = (rpoly (k,a)) . k by XREAL_0:def 2
.= 1_ R by HURWITZ:25
.= 1. R ;
:: thesis: verum