:: deftheorem Def19 defines IotaMap LMODFREE:def 19 :
for R being non degenerated Ring
for X being non empty set
for b₃ being Function of X,(Free_LMod (X,R)) holds
( b₃ = IotaMap (X,R) iff for x being Element of X holds b₃ . x = Iota (x,R) );