theorem Th13: :: LIOUVIL2:12

for R being non degenerated Ring
for S being Subring of R
for f being Polynomial of S
for g being non-zero Polynomial of R st f = g holds
f is non-zero