theorem lemadd2: :: VECTSP13:11

for F being Field
for U, V being VectSp of F
for B being non empty finite Subset of U
for b being Element of B
for f being Function of B,V
for l being Linear_Combination of B st Carrier l = {b} holds
( Carrier (f (#) l) = {(f . b)} & Sum (f (#) l) = (l . b) * (f . b) )