theorem lemadd2a: :: VECTSP13:10

for F being Field
for U, V being VectSp of F
for B being non empty finite Subset of U
for f being Function of B,V
for l being Linear_Combination of B holds Carrier (f (#) l) c= f .: (Carrier l)