for R being Ring
for V being VectSp of R
for A1, A2 being Subset of V
for l being Linear_Combination of A1 \/ A2 st A1 /\ A2 = {} holds
ex l1 being Linear_Combination of A1 ex l2 being Linear_Combination of A2 st l = l1 + l2