for R being Ring
for S being RingExtension of R
for p being Polynomial of R holds p is Polynomial of S