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