theorem :: ALGNUM_1:22

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