theorem Th37: :: E_TRANS1:35

for F being domRing
for E being RingExtension of F
for p being Polynomial of F
for q being Polynomial of E
for a being Element of F
for b being Element of E st p = q & a = b holds
a * p = b * q