theorem Th6: :: FIELD_4:10

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