now

let n be Nat; :: thesis: ( n >= len p implies (NormPolynomial p) . n = 0. L )
assume A1: n >= len p ; :: thesis: (NormPolynomial p) . n = 0. L
reconsider nn = n as Element of NAT by ORDINAL1:def 13;
thus (NormPolynomial p) . n = (p . nn) / (p . ((len p) -' 1)) by Def10
.= (0. L) / (p . ((len p) -' 1)) by A1, ALGSEQ_1:22
.= (0. L) * ((p . ((len p) -' 1)) " ) by VECTSP_1:def 23
.= 0. L by VECTSP_1:39 ; :: thesis: verum

end;

hence NormPolynomial p is finite-Support by ALGSEQ_1:def 2; :: thesis: verum