:: deftheorem defK defines (#) VECTSP13:def 2 :
for F being Field
for U, V being VectSp of F
for B being non empty finite Subset of U
for l being Linear_Combination of B
for f being Function of B,V
for b₇ being Linear_Combination of rng f holds
( b₇ = f (#) l iff for v being Element of V holds b₇ . v = Sum (Expand (f,l,v)) );