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