reconsider p1 = p as Element of 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