theorem ThTF3C2: :: ZMODUL05:42

for R being Ring
for V being LeftMod of R
for A, B being finite Subset of V
for l being Linear_Combination of V
for l0, l1, l2 being FinSequence of R st A /\ B = {} & l0 = l * (canFS (A \/ B)) & l1 = l * (canFS A) & l2 = l * (canFS B) holds
Sum l0 = (Sum l1) + (Sum l2)