theorem lemminusx: :: VECTSP13:15

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 l1, l2, l3 being Linear_Combination of B st l3 = l1 - l2 holds
f (#) l3 = (f (#) l1) - (f (#) l2)