f . p is Element of (Polynom-Ring R) ;
hence f . p is Element of the carrier of (Polynom-Ring R) ; :: thesis: verum