for R being Ring
for S being RingExtension of R holds the carrier of (Polynom-Ring R) c= the carrier of (Polynom-Ring S)