:: deftheorem Def31 defines Phi LMODFREE:def 31 :
for R being non degenerated Ring
for X being non empty set
for N being LeftMod of R
for v being Function of X, the carrier of N
for b₅ being Function of (Free_LMod (X,R)), the carrier of N holds
( b₅ = Phi v iff for f being Element of (Free_LMod (X,R)) holds b₅ . f = PhiSet (v,f,(SuppFin f)) );