let F be Field; :: thesis: for p being Element of the carrier of (Polynom-Ring F) holds deg (NormPolynomial p) = deg p
let p be Element of the carrier of (Polynom-Ring F); :: thesis: deg (NormPolynomial p) = deg p

per cases ( p = 0_. F or p <> 0_. F ) ;

suppose p = 0_. F ; :: thesis: deg (NormPolynomial p) = deg p

hence deg (NormPolynomial p) = deg p by RING_4:22; :: thesis: verum

end;

suppose p <> 0_. F ; :: thesis: deg (NormPolynomial p) = deg p

then len (NormPolynomial p) = len p by POLYNOM4:5, POLYNOM5:57;
hence deg (NormPolynomial p) = (len p) - 1 by HURWITZ:def 2
.= deg p by HURWITZ:def 2 ;
:: thesis: verum

end;

end;