theorem lembas1: :: VECTSP13:4

for F being Field
for U being VectSp of F
for B being linearly-independent Subset of U
for w being Element of U st w in B holds
for l being Linear_Combination of B st Sum l = w holds
( Carrier l = {w} & l . w = 1. F )