:: deftheorem defines Expand VECTSP13:def 1 :
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 v being Element of V holds Expand (f,l,v) = l * (canFS (f " {v}));