theorem constpol: :: FIELD_6:23

for R being Ring
for S being RingExtension of R
for a being Element of R
for b being Element of S st a = b holds
a | R = b | S