for R being Ring
for S being RingExtension of R holds Polynom-Ring S is RingExtension of Polynom-Ring R ;