theorem lemaddx: :: VECTSP13:12

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)