theorem :: RLVECT_2:39

for V being non empty addLoopStr
for L1, L2 being Linear_Combination of V holds L1 + L2 = L2 + L1 ;