let F be Field; :: thesis: for p being non zero Element of the carrier of (Polynom-Ring F) holds NormPolynomial p = ((LC p) ") * p
let p be non zero Element of the carrier of (Polynom-Ring F); :: thesis: NormPolynomial p = ((LC p) ") * p

now :: thesis: for x being object st x in NAT holds
(((LC p) ") * p) . x = (NormPolynomial p) . x

let x be object ; :: thesis: ( x in NAT implies (((LC p) ") * p) . x = (NormPolynomial p) . x )
assume x in NAT ; :: thesis: (((LC p) ") * p) . x = (NormPolynomial p) . x
then reconsider i = x as Element of NAT ;
thus (((LC p) ") * p) . x = ((LC p) ") * (p . i) by POLYNOM5:def 4
.= (p . i) / (p . ((len p) -' 1))
.= (NormPolynomial p) . x by POLYNOM5:def 11 ; :: thesis: verum

end;

hence NormPolynomial p = ((LC p) ") * p by FUNCT_2:12; :: thesis: verum