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