theorem Th10: :: LMODFREE:11

for X being non empty set
for R being non degenerated Ring
for N0 being Nat
for F being FinSequence of the carrier of (Free_LMod (X,R))
for x being Element of X st len F = N0 + 1 holds
ev_ (F,x) = (ev_ ((F | N0),x)) ^ <*((ev_ (x,R)) . (F /. (len F)))*>