:: deftheorem defK1 defines (#) VECTSP13:def 3 :
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 rng f
for b₇ being Linear_Combination of B holds
( b₇ = l (#) f iff for u being Element of U st u in B holds
b₇ . u = l . (f . u) );