for F being Field holds NormPolynomial (0_. F) = 0_. F