for V being RealLinearSpace
for L1, L2 being Linear_Combination of V holds sum (L1 - L2) = (sum L1) - (sum L2)