:: deftheorem Def28 defines TermFS LMODFREE:def 28 :
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 f being Element of (Free_LMod (X,R))
for b₆ being Function of X, the carrier of N holds
( b₆ = TermFS (f,v) iff for x being Element of X holds b₆ . x = ((@ f) . x) * (v . x) );