theorem Th12: :: LMODFREE:13

for X being non empty set
for R being non degenerated Ring
for f being Element of (Free_LMod (X,R))
for x being Element of X st not x in Support (@ f) holds
0. R = (@ (Sum (F_idxseq f))) . x