set q = NormPolynomial p;
A1: p <> 0_. L ;
then (NormPolynomial p) . ((len p) -' 1) = 1. L by POLYNOM4:5, POLYNOM5:56;
then LC (NormPolynomial p) = 1. L by A1, POLYNOM4:5, POLYNOM5:57;
hence NormPolynomial p is normalized ; :: thesis: verum