reconsider n = n as Element of NAT by ORDINAL1:def 12;
reconsider p1 = p as Element of (Polynom-Ring L) by POLYNOM3:def 10;
(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 10; :: thesis: verum