theorem Th29: :: VECTSP_6:29

for GF being Field
for V being VectSp of GF
for a being Element of GF
for L being Linear_Combination of V st a <> 0. GF holds
Carrier (a * L) = Carrier L