now :: thesis: for n being Nat st n >= len p holds
(NormPolynomial p) . n = 0. L

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 12;
thus (NormPolynomial p) . n = (p . nn) / (p . ((len p) -' 1)) by Def11
.= (0. L) / (p . ((len p) -' 1)) by A1, ALGSEQ_1:8
.= (0. L) * ((p . ((len p) -' 1)) ")
.= 0. L ; :: thesis: verum

end;

hence NormPolynomial p is finite-Support ; :: thesis: verum