theorem :: CONVEX4:21
for V being non empty addLoopStr
for L1, L2 being C_Linear_Combination of V holds L1 + L2 = L2 + L1 ;