:: deftheorem dh defines hom_Ext_eval FIELD_13:def 2 :
for n being Nat
for R, S being non degenerated comRing
for x being Function of n,S
for b₅ being Function of (Polynom-Ring (n,R)),S holds
( b₅ = hom_Ext_eval (x,R) iff for p being Polynomial of n,R holds b₅ . p = Ext_eval (p,x) );