:: deftheorem Def23 defines ev_ LMODFREE:def 23 :
for X being non empty set
for R being non degenerated Ring
for s being FinSequence of the carrier of (Free_LMod (X,R))
for x being Element of X
for b₅ being FinSequence of the carrier of R holds
( b₅ = ev_ (s,x) iff ( dom b₅ = dom s & ( for i being Nat st i in dom s holds
b₅ . i = (ev_ (x,R)) . (s /. i) ) ) );