theorem :: ZMODUL05:49

for R being Ring
for V being LeftMod of R
for A being Subset of V
for l1, l2 being Linear_Combination of A st Carrier l1 misses Carrier l2 holds
Carrier (l1 - l2) = (Carrier l1) \/ (Carrier l2)