:: deftheorem Def21 defines ev_iota LMODFREE:def 21 :
for X being non empty set
for R being non degenerated Ring
for f being Element of (Free_LMod (X,R))
for b₄ being Function of X,(Free_LMod (X,R)) holds
( b₄ = ev_iota f iff for x being Element of X holds b₄ . x = ((ev_ (x,R)) . f) * ((IotaMap (X,R)) . x) );