theorem ThTF3C3: :: ZMODUL05:43

for R being Ring
for V being LeftMod of R
for A being finite Subset of V
for l, l0 being Linear_Combination of V st l | (Carrier l0) = l0 | (Carrier l0) & Carrier l0 c= Carrier l & A c= Carrier l0 holds
Sum (l * (canFS A)) = Sum (l0 * (canFS A))