set PR = Polynom-Ring (n,R);
reconsider P = p as Element of (Polynom-Ring (n,R)) by POLYNOM1:def 11;
(power (Polynom-Ring (n,R))) . (P,k) in the carrier of (Polynom-Ring (n,R)) ;
hence (power (Polynom-Ring (n,R))) . (p,k) is Polynomial of n,R by POLYNOM1:def 11; :: thesis: verum