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