theorem Th25: :: ALGNUM_1:21

for A, B being Ring
for x being Element of B
for z0 being Element of A st A is Subring of B holds
Ext_eval (<%z0%>,x) = In (z0,B)