theorem Th5: :: FIELD_4:8

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