theorem Th13: :: FIELD_4:18

for R, S being Ring st S is RingExtension of R holds
the multF of (Polynom-Ring R) = the multF of (Polynom-Ring S) || the carrier of (Polynom-Ring R)