:: deftheorem Def9 defines hom_Ext_eval ALGNUM_1:def 11 :
for A, B being Ring
for x being Element of B
for b₄ being Function of (Polynom-Ring A),B holds
( b₄ = hom_Ext_eval (x,A) iff for p being Polynomial of A holds b₄ . p = Ext_eval (p,x) );