theorem Th11: :: LMODFREE:12

for X being non empty set
for R being non degenerated Ring
for F being FinSequence of the carrier of (Free_LMod (X,R))
for x being Element of X holds (ev_ (x,R)) . (Sum F) = Sum (ev_ (F,x))