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