:: deftheorem Def20 defines ev_ LMODFREE:def 20 :
for R being non degenerated Ring
for X being non empty set
for x being Element of X
for b₄ being Function of (Free_LMod (X,R)),R holds
( b₄ = ev_ (x,R) iff for f being Element of (Free_LMod (X,R)) holds b₄ . f = (@ f) . x );