theorem lembas: :: VECTSP13:16

for F being Field
for U, V being VectSp of F
for B being non empty finite Subset of U st B is linearly-independent holds
for w being Element of U st w in B holds
for l being Linear_Combination of B st Sum l = w holds
for f being Function of B,V holds Sum (f (#) l) = f . w