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