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)