theorem npl0: :: RING_4:22

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