for GF being Field
for V being VectSp of GF
for L being Linear_Combination of V
for a being Element of GF holds Sum (a * L) = a * (Sum L)