theorem :: FIELD_4:9

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