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