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

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