theorem Th11: :: FIELD_4:16

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