theorem lemdeg: :: REALALG3:11

for F being Field
for p being Element of the carrier of (Polynom-Ring F) holds deg (NormPolynomial p) = deg p