let F be Field; :: thesis:
set q = 0_. F;
set p = NormPolynomial (0_. F);

let x be object ; :: thesis:
assume x in NAT ; :: thesis:
then reconsider i = x as Element of NAT ;
(NormPolynomial (0_. F)) . i = ((0_. F) . i) / ((0_. F) . ((len (0_. F)) -' 1)) by POLYNOM5:def 11
.= (0. F) * (((0_. F) . ((len (0_. F)) -' 1)) ") by FUNCOP_1:7
.= (0_. F) . i by FUNCOP_1:7 ;
hence (NormPolynomial (0_. F)) . x = (0_. F) . x ; :: thesis:

end;