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