theorem Th7: :: NORMSP_4:6

for X being non empty addLoopStr
for A, B being Subset of X
for l1 being Linear_Combination of A
for l2 being Linear_Combination of B st A misses B holds
ex l being Linear_Combination of A \/ B st
( Carrier l = (Carrier l1) \/ (Carrier l2) & l = l1 + l2 )