theorem lemmultx: :: VECTSP13:13

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 being Linear_Combination of B
for a being Element of F st l2 = a * l1 holds
f (#) l2 = a * (f (#) l1)