:: deftheorem Def17 defines iota LMODFREE:def 17 :
for X being non empty set
for R being non degenerated Ring
for a being Element of X
for b₄ being Function of X,([#] R) holds
( b₄ = iota (a,R) iff for x being object st x in X holds
( ( x = a implies b₄ . x = 1. R ) & ( x <> a implies b₄ . x = 0. R ) ) );