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