theorem Th8: :: LIOUVIL2:7
for R being Ring
for S being Subring of R
for f being Polynomial of S holds f is Polynomial of R