reconsider n = n as Element of NAT by ORDINAL1:def 12;
reconsider p1 = p as Element of (Polynom-Ring L) by POLYNOM3:def 10;
(power (Polynom-Ring L)) . (p1,n) is Polynomial of L by POLYNOM3:def 10;
hence p `^ n is finite-Support ; :: thesis: verum