theorem Th18: :: LIOUVIL2:17

for R being Ring
for S being Subring of R
for r being Element of R
for s being Element of S
for f being Polynomial of R
for g being Polynomial of S st r = s & f = g & r is_a_root_of f holds
s is_a_root_of g